﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using OverSATbLib;
using System.Numerics;

namespace OverSATbTest
{
    [TestClass]

    public class SolverTests
    {
        [TestMethod]
        public void SolveSingleClause()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new []{ 3, 2, -1 });

            var t1 = solver.GetValueAtRow(1);
            Assert.AreEqual("3=1, 2=0, 1=0", t1.ToString(), "Row 1 must match");
            var t2 = solver.GetValueAtRow(4);
            Assert.AreEqual("3=0, 2=0, 1=1", t2.ToString(), "Row 4 must match");
            var t3 = solver.GetValueAtRow(5);
            Assert.AreEqual("3=1, 2=0, 1=1", t3.ToString(), "Row 5 must match");
            var t4 = solver.GetValueAtRow(7);
            Assert.AreEqual("3=1, 2=1, 1=1", t4.ToString(), "Row 7 must match");

            Assert.AreEqual(1, solver.DeletedTuples.Count);
            Assert.AreEqual("1=1, 2=0, 3=0", solver.DeletedTuples[0].ToString(), "Deleted tuple must match");
            string deletedTuple = solver.DeletedTuples[0].ToString();

            string resultString = solver.GetTrueValues(10).ToPrettyString();
            string bruteForceControlString = solver.GetTrueValuesBruteForce(10).ToPrettyString();

            Assert.AreEqual(bruteForceControlString, resultString, "Solved must equal brute force solution");

            string control =
@"3=0, 2=0, 1=0
3=1, 2=0, 1=0
3=0, 2=1, 1=0
3=1, 2=1, 1=0
3=1, 2=0, 1=1
3=0, 2=1, 1=1
3=1, 2=1, 1=1";

            Assert.AreEqual(control, resultString, "Result must equal control");

        }

        [TestMethod]
        public void SolveDoubleClauseFourVariable()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new[] { 3, 2, -1 });
            solver.AddClause(new[] { -4, -3, 1 });

            var deleteCount = solver.DeletedTuples.Count;

            Assert.AreEqual(2, deleteCount, "Should have 2 deletes");

            var bruteForceControl = solver.GetTrueValuesBruteForce(16);

            Assert.AreEqual(12, bruteForceControl.Count, "Expecting 12 solution rows.");
            var bruteForceControlString = bruteForceControl.ToPrettyString();

            var testControl = solver.GetTrueValues(16);
            var testControlString = testControl.ToPrettyString();

            Assert.AreEqual(bruteForceControlString, testControlString, "Results should be equal between brute force and control.");
        }

        [TestMethod]
        public void AddErroneousClausesToSolver()
        {
            SatSolver solver = new SatSolver();
            int exceptionCount = 0;

            try
            {
                solver.AddClause(new[] { 3, 2, -1, 1 });
            }
            catch (ClauseHasDuplicateVariablesExeption exc)
            {
                exceptionCount++;
            }

            try
            {
                solver.AddClause(new[] { 3, 2, -1, 3 });
            }
            catch (ClauseHasDuplicateVariablesExeption exc)
            {
                exceptionCount++;

            }

            try
            {
                solver.AddClause(new[] { -3, 2, -1, 3 });
            }
            catch (ClauseHasDuplicateVariablesExeption exc)
            {
                exceptionCount++;

            }

            try
            {
                solver.AddClause(new[] { -3, 2, -1, 3, 1 });
            }
            catch (ClauseHasDuplicateVariablesExeption exc)
            {
                exceptionCount++;
            }

            try
            {
                solver.AddClause(new[] { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33 });
            }
            catch (ClauseHasTooManyVariablesException exc)
            {
                exceptionCount++;
            }

            try
            {
                solver.AddClause(new[] { 1, 2, 3 });
            }
            catch (System.Exception exc)
            {
                exceptionCount++;
            }

            Assert.IsTrue(exceptionCount == 5, "Must accurately produce ClauseXXX exceptions");
        }

        [TestMethod]
        public void RoundTripDoubleToString()
        {
            double t = 1234.1234567890123456789D;
            var s = t.ToString("R");
        }

        [TestMethod]
        public void SolveSimpleCNF1()
        {
            string cnfString =
@"c  simple_v3_c2.cnf
c
p cnf 3 2
3 -2 0
2 3 -1 0
";
            string f = CNFSatSolver.SolveCNFString(cnfString, 8);
            Assert.IsFalse(string.IsNullOrEmpty(f), "Results from solver1.");

        }

        [TestMethod]
        public void QuinnsCNF()
        {
            string cnfString =
            @"c quinn.cnf
c
p cnf 16 18
  1    2  0
  3    4  0
 - 2 - 4  0
 - 4 - 5  0
  5 - 6  0
  6 -7  0
  6    7  0
  8 - 9  0
  9   10  0
  9 - 10  0
- 10 - 11  0
 10   12  0
 11   12  0
 13   14  0
 14 - 15  0
 15   16  0
  7 - 16  0
- 8 - 14  0
";

            string f = CNFSatSolver.SolveCNFString(cnfString, 1);
            Assert.IsFalse(string.IsNullOrEmpty(f), "Results from quinn.");

            string control =
            @"c OverSATb 1 solutions
s cnf 1 16 18
v 1 -2 3 -4 5 6 7 8 9 -10 -11 12 13 -14 -15 16 0
";
            Assert.IsTrue(f == control, "Results match.");
        }

        [TestMethod]
        public void SolveSimpleCNF2()
        {
            string cnfString =
@"c  simple_v3_c2.cnf
c
p cnf 4 2
3 2 -1 0
-4 -3 1 0
";
            string f = CNFSatSolver.SolveCNFString(cnfString, 20);

            string control =
@"c OverSATb 12 solutions
s cnf 1 4 2
v -3 -2 -1 -4 0
v 3 -2 -1 -4 0
v -3 2 -1 -4 0
v 3 2 -1 -4 0
v 3 -2 1 -4 0
v -3 2 1 -4 0
v 3 2 1 -4 0
v -3 -2 -1 4 0
v -3 2 -1 4 0
v 3 -2 1 4 0
v -3 2 1 4 0
v 3 2 1 4 0
";
            Assert.IsFalse(string.IsNullOrEmpty(f), "Results from solver1.");
            Assert.IsTrue(f == control, "Results match.");

        }

        /* Problems from */
/* http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html */
        [TestMethod]
        public void SolveNoSolutionsRealCNF()
        {
            string problem =
            @"c FILE: aim-100-1_6-no-1.cnf
c
c SOURCE: Kazuo Iwama, Eiji Miyano (miyano@cscu.kyushu-u.ac.jp),
c          and Yuichi Asahiro
c
c DESCRIPTION: Artifical instances from generator by source.  Generators
c              and more information in sat/contributed/iwama.
c
c NOTE: Not Satisfiable
c
p cnf 100 160
16 30 95 0
-16 30 95 0
-30 35 78 0
-30 -78 85 0
-78 -85 95 0
8 55 100 0
8 55 -95 0
9 52 100 0
9 73 -100 0
-8 -9 52 0
38 66 83 0
-38 83 87 0
-52 83 -87 0
66 74 -83 0
-52 -66 89 0
-52 73 -89 0
-52 73 -74 0
-8 -73 -95 0
40 -55 90 0
-40 -55 90 0
25 35 82 0
-25 82 -90 0
-55 -82 -90 0
11 75 84 0
11 -75 96 0
23 -75 -96 0
-11 23 -35 0
-23 29 65 0
29 -35 -65 0
-23 -29 84 0
-35 54 70 0
-54 70 77 0
19 -77 -84 0
-19 -54 70 0
22 68 81 0
-22 48 81 0
-22 -48 93 0
3 -48 -93 0
7 18 -81 0
-7 56 -81 0
3 18 -56 0
-18 47 68 0
-18 -47 -81 0
-3 68 77 0
-3 -77 -84 0
19 -68 -70 0
-19 -68 74 0
-68 -70 -74 0
54 61 -62 0
50 53 -62 0
-50 61 -62 0
-27 56 93 0
4 14 76 0
4 -76 96 0
-4 14 80 0
-14 -68 80 0
-10 -39 -89 0
1 49 -81 0
1 26 -49 0
17 -26 -49 0
-1 17 -40 0
16 51 -89 0
-9 57 60 0
12 45 -51 0
2 12 69 0
2 -12 40 0
-12 -51 69 0
-33 60 -98 0
5 -32 -66 0
2 -47 -100 0
-42 64 83 0
20 -42 -64 0
20 -48 98 0
-20 50 98 0
-32 -50 98 0
-24 37 -73 0
-24 -37 -100 0
-57 71 81 0
-37 40 -91 0
31 42 81 0
-31 42 72 0
-31 42 -72 0
7 -19 25 0
-1 -25 -94 0
-15 -44 79 0
-6 31 46 0
-39 41 88 0
28 -39 43 0
28 -43 -88 0
-4 -28 -88 0
-30 -39 -41 0
-29 33 88 0
-16 21 94 0
-10 26 62 0
-11 -64 86 0
-6 -41 76 0
38 -46 93 0
26 -37 94 0
-26 53 -79 0
78 87 -94 0
65 76 -87 0
23 51 -62 0
-11 -36 57 0
41 59 -65 0
-56 72 -91 0
13 -20 -46 0
-13 15 79 0
-17 47 -60 0
-13 -44 99 0
-7 -38 67 0
37 -49 62 0
-14 -17 -79 0
-13 -15 -22 0
32 -33 -34 0
24 45 48 0
21 24 -48 0
-36 64 -85 0
10 -61 67 0
-5 44 59 0
-80 -85 -99 0
6 37 -97 0
-21 -34 64 0
-5 44 46 0
58 -76 97 0
-21 -36 75 0
-15 58 -59 0
-58 -76 -99 0
-2 15 33 0
-26 34 -57 0
-18 -82 -92 0
27 -80 -97 0
6 32 63 0
-34 -86 92 0
13 -61 97 0
-28 43 -98 0
5 39 -86 0
39 -45 92 0
27 -43 97 0
13 -58 -86 0
-28 -67 -93 0
-69 85 99 0
42 71 -72 0
10 -27 -63 0
-59 63 -83 0
36 86 -96 0
-2 36 75 0
-59 -71 89 0
36 -67 91 0
36 -60 63 0
-63 91 -93 0
25 87 92 0
-21 49 -71 0
-2 10 22 0
6 -18 41 0
6 71 -92 0
-53 -69 -71 0
-2 -53 -58 0
43 -45 -96 0
34 -45 -69 0
63 -86 -98 0
";

            var solution = CNFSatSolver.SolveCNFString(problem, 5);
            var control =
            @"c OverSATb 0 solutions
s cnf 0 100 160
";
            Assert.IsTrue(solution == control, "SAT problem must have 0 solutions");

        }

        [TestMethod]
        public void SolveNemesisCNF()
        {
            string problem =
            @"c FILE:  bf0432-007.cnf
c
c SOURCE: Allen Van Gelder (avg@cs.ucsd.edu) and Yumi Tsuji
c        (tsuji@cse.ucsc.edu) 
c
c Nemesis formula in 6CNF in accordance with DIMACS CNF format:
c    Filename: MCNC/c432/c432.tdl
c    Formula number 7
c    1317 variables (range: 2 - 1318)
c    3668 clauses
c
c p cnf 1318 3668
p cnf 1040 3668
700	0
-985	0
1039	0
700	0
-701	0
699	0
663	-664	0
-663	664	0
699	701	0
-699	-701	0
-667	-706	0
-665	-706	0
-669	-706	0
699	663	0
-699	-663	0
985	-701	0
-985	701	0
985	-664	0
-985	664	0
701	-664	0
-701	664	0
-39	-988	0
37	-988	0
39	-989	0
-37	-989	0
-989	987	0
-988	987	0
201	37	0
-201	-37	0
-202	38	0
203	39	0
-203	-39	0
207	201	0
-207	-201	0
-208	202	0
209	203	0
-209	-203	0
62	-204	0
-62	204	0
62	-207	0
-62	207	0
62	-214	0
-62	214	0
62	-259	0
-62	259	0
62	-288	0
-62	288	0
62	-436	0
-62	436	0
62	-495	0
-62	495	0
62	-544	0
-62	544	0
62	-597	0
-62	597	0
62	-639	0
-62	639	0
62	-708	0
-62	708	0
62	-736	0
-62	736	0
62	-762	0
-62	762	0
62	-778	0
-62	778	0
62	-827	0
-62	827	0
62	-838	0
-62	838	0
62	-854	0
-62	854	0
62	-914	0
-62	914	0
62	-949	0
-62	949	0
63	-205	0
63	-208	0
63	-215	0
63	-260	0
63	-289	0
63	-437	0
63	-496	0
63	-545	0
63	-598	0
63	-640	0
63	-709	0
63	-737	0
63	-763	0
63	-779	0
63	-828	0
63	-839	0
63	-855	0
63	-915	0
63	-950	0
64	-206	0
-64	206	0
64	-209	0
-64	209	0
64	-216	0
-64	216	0
64	-261	0
-64	261	0
64	-290	0
-64	290	0
64	-438	0
-64	438	0
64	-497	0
-64	497	0
64	-546	0
-64	546	0
64	-599	0
-64	599	0
64	-641	0
-64	641	0
64	-710	0
-64	710	0
64	-738	0
-64	738	0
64	-764	0
-64	764	0
64	-780	0
-64	780	0
64	-829	0
-64	829	0
64	-840	0
-64	840	0
64	-856	0
-64	856	0
64	-916	0
-64	916	0
64	-951	0
-64	951	0
699	62	0
663	62	0
65	62	0
685	62	0
701	64	0
663	64	0
65	64	0
685	64	0
836	685	0
-836	-685	0
686	-836	0
-686	836	0
686	-837	0
-686	837	0
-884	-686	0
-885	-686	0
690	-697	0
-690	697	0
690	-698	0
-690	698	0
690	-730	0
-690	730	0
690	-885	0
-690	885	0
26	690	0
-26	-690	0
7	-881	0
-7	881	0
7	-884	0
-7	884	0
-286	-65	0
-68	-65	0
61	-67	0
-61	67	0
61	-68	0
-61	68	0
-547	-61	0
-533	-61	0
514	-533	0
-514	533	0
514	-534	0
-514	534	0
536	514	0
-536	-514	0
32	-536	0
-32	536	0
32	-537	0
-32	537	0
32	-568	0
-32	568	0
5	-547	0
-5	547	0
5	-548	0
-5	548	0
66	-286	0
-66	286	0
66	-287	0
-66	287	0
-857	-66	0
-850	-66	0
841	-848	0
-841	848	0
841	-849	0
-841	849	0
841	-850	0
-841	850	0
841	-878	0
-841	878	0
9	841	0
-9	-841	0
21	-857	0
-21	857	0
21	-858	0
-21	858	0
-667	-663	0
-665	-663	0
-669	-663	0
494	-668	0
-494	668	0
494	-669	0
-494	669	0
-512	-494	0
-513	-494	0
470	-490	0
-470	490	0
470	-493	0
-470	493	0
470	-508	0
-470	508	0
470	-513	0
-470	513	0
34	470	0
-34	-470	0
25	-509	0
-25	509	0
25	-512	0
-25	512	0
796	665	0
781	665	0
797	665	0
947	797	0
-947	-797	0
926	-947	0
-926	947	0
926	-948	0
-926	948	0
-945	-926	0
-946	-926	0
927	-938	0
-927	938	0
927	-941	0
-927	941	0
927	-946	0
-927	946	0
927	-962	0
-927	962	0
19	927	0
-19	-927	0
17	-942	0
-17	942	0
17	-945	0
-17	945	0
783	781	0
-783	-781	0
777	-782	0
-777	782	0
777	-783	0
-777	783	0
-924	-777	0
-925	-777	0
587	-917	0
-587	917	0
587	-918	0
-587	918	0
587	-925	0
-587	925	0
910	587	0
-910	-587	0
35	-909	0
-35	909	0
35	-910	0
-35	910	0
30	-921	0
-30	921	0
30	-924	0
-30	924	0
799	796	0
-799	-796	0
213	-798	0
-213	798	0
213	-799	0
-213	799	0
-775	-213	0
-776	-213	0
220	-233	0
-220	233	0
220	-234	0
-220	234	0
220	-424	0
-220	424	0
220	-776	0
-220	776	0
28	220	0
-28	-220	0
4	-772	0
-4	772	0
4	-775	0
-4	775	0
591	-666	0
-591	666	0
591	-667	0
-591	667	0
-600	-591	0
-593	-591	0
580	-592	0
-580	592	0
580	-593	0
-580	593	0
627	580	0
-627	-580	0
6	-627	0
-6	627	0
6	-628	0
-6	628	0
6	-638	0
-6	638	0
10	-600	0
-10	600	0
10	-601	0
-10	601	0
706	699	0
-706	-699	0
702	-706	0
-702	706	0
702	-707	0
-702	707	0
-889	-702	0
-890	-702	0
711	-718	0
-711	718	0
711	-719	0
-711	719	0
711	-756	0
-711	756	0
711	-890	0
-711	890	0
27	711	0
-27	-711	0
11	-886	0
-11	886	0
11	-889	0
-11	889	0
-42	-995	0
40	-995	0
42	-996	0
-40	-996	0
-996	994	0
-995	994	0
657	40	0
-657	-40	0
-658	41	0
659	42	0
-659	-42	0
195	-657	0
-195	657	0
195	-660	0
-195	660	0
195	-676	0
-195	676	0
196	-658	0
196	-661	0
196	-677	0
197	-659	0
-197	659	0
197	-662	0
-197	662	0
197	-678	0
-197	678	0
250	195	0
-250	-195	0
-251	196	0
252	197	0
-252	-197	0
87	-235	0
-87	235	0
87	-238	0
-87	238	0
87	-250	0
-87	250	0
87	-262	0
-87	262	0
87	-271	0
-87	271	0
87	-309	0
-87	309	0
87	-315	0
-87	315	0
87	-324	0
-87	324	0
87	-339	0
-87	339	0
87	-439	0
-87	439	0
87	-521	0
-87	521	0
87	-551	0
-87	551	0
87	-604	0
-87	604	0
87	-620	0
-87	620	0
87	-739	0
-87	739	0
87	-765	0
-87	765	0
87	-793	0
-87	793	0
87	-824	0
-87	824	0
87	-830	0
-87	830	0
87	-861	0
-87	861	0
87	-901	0
-87	901	0
88	-236	0
88	-239	0
88	-251	0
88	-263	0
88	-272	0
88	-310	0
88	-316	0
88	-325	0
88	-340	0
88	-440	0
88	-522	0
88	-552	0
88	-605	0
88	-621	0
88	-740	0
88	-766	0
88	-794	0
88	-825	0
88	-831	0
88	-862	0
88	-902	0
89	-237	0
-89	237	0
89	-240	0
-89	240	0
89	-252	0
-89	252	0
89	-264	0
-89	264	0
89	-273	0
-89	273	0
89	-311	0
-89	311	0
89	-317	0
-89	317	0
89	-326	0
-89	326	0
89	-341	0
-89	341	0
89	-441	0
-89	441	0
89	-523	0
-89	523	0
89	-553	0
-89	553	0
89	-606	0
-89	606	0
89	-622	0
-89	622	0
89	-741	0
-89	741	0
89	-767	0
-89	767	0
89	-795	0
-89	795	0
89	-826	0
-89	826	0
89	-832	0
-89	832	0
89	-863	0
-89	863	0
89	-903	0
-89	903	0
108	87	0
651	87	0
446	87	0
464	87	0
-109	88	0
-652	88	0
-447	88	0
-465	88	0
110	89	0
653	89	0
448	89	0
466	89	0
480	464	0
-480	-464	0
-481	465	0
482	466	0
-482	-466	0
268	-477	0
-268	477	0
268	-480	0
-268	480	0
269	-478	0
269	-481	0
270	-479	0
-270	479	0
270	-482	0
-270	482	0
-498	-268	0
-489	-268	0
-493	-268	0
-499	269	0
-499	-493	0
-499	-489	0
-500	-270	0
-489	-270	0
-493	-270	0
12	-486	0
-12	486	0
12	-489	0
-12	489	0
483	-498	0
-483	498	0
483	-501	0
-483	501	0
484	-499	0
484	-502	0
485	-500	0
-485	500	0
485	-503	0
-485	503	0
-668	-975	0
495	-975	0
668	-976	0
-495	-976	0
-976	483	0
-975	483	0
-496	484	0
-668	-1001	0
497	-1001	0
668	-1002	0
-497	-1002	0
-1002	485	0
-1001	485	0
-458	-446	0
-787	-446	0
-679	-446	0
-459	447	0
-788	447	0
-680	447	0
-460	-448	0
-789	-448	0
-681	-448	0
452	-679	0
-452	679	0
452	-682	0
-452	682	0
452	-821	0
-452	821	0
453	-680	0
453	-683	0
453	-822	0
454	-681	0
-454	681	0
454	-684	0
-454	684	0
454	-823	0
-454	823	0
-952	-452	0
-937	-452	0
-941	-452	0
-953	453	0
-953	-941	0
-953	-937	0
-954	-454	0
-937	-454	0
-941	-454	0
18	-934	0
-18	934	0
18	-937	0
-18	937	0
931	-952	0
-931	952	0
931	-955	0
-931	955	0
932	-953	0
932	-956	0
933	-954	0
-933	954	0
933	-957	0
-933	957	0
-948	-963	0
949	-963	0
948	-964	0
-949	-964	0
-964	931	0
-963	931	0
-950	932	0
-948	-1003	0
951	-1003	0
948	-1004	0
-951	-1004	0
-1004	933	0
-1003	933	0
449	-787	0
-449	787	0
449	-790	0
-449	790	0
450	-788	0
450	-791	0
451	-789	0
-451	789	0
451	-792	0
-451	792	0
-806	-449	0
-897	-449	0
-917	-449	0
-807	450	0
-807	-917	0
-807	-897	0
-808	-451	0
-897	-451	0
-917	-451	0
22	-897	0
-22	897	0
22	-898	0
-22	898	0
584	-806	0
-584	806	0
584	-809	0
-584	809	0
585	-807	0
585	-810	0
586	-808	0
-586	808	0
586	-811	0
-586	811	0
-782	-969	0
778	-969	0
782	-970	0
-778	-970	0
-970	584	0
-969	584	0
-779	585	0
-782	-1005	0
780	-1005	0
782	-1006	0
-780	-1006	0
-1006	586	0
-1005	586	0
217	-455	0
-217	455	0
217	-458	0
-217	458	0
218	-456	0
218	-459	0
219	-457	0
-219	457	0
219	-460	0
-219	460	0
-227	-217	0
-442	-217	0
-233	-217	0
-228	218	0
-228	-233	0
-228	-442	0
-229	-219	0
-442	-219	0
-233	-219	0
23	-442	0
-23	442	0
23	-443	0
-23	443	0
210	-227	0
-210	227	0
210	-230	0
-210	230	0
211	-228	0
211	-231	0
212	-229	0
-212	229	0
212	-232	0
-212	232	0
-798	-981	0
214	-981	0
798	-982	0
-214	-982	0
-982	210	0
-981	210	0
-215	211	0
-798	-1007	0
216	-1007	0
798	-1008	0
-216	-1008	0
-1008	212	0
-1007	212	0
461	-651	0
-461	651	0
461	-654	0
-461	654	0
462	-652	0
462	-655	0
463	-653	0
-463	653	0
463	-656	0
-463	656	0
614	461	0
-614	-461	0
-615	462	0
616	463	0
-616	-463	0
581	-614	0
-581	614	0
581	-617	0
-581	617	0
582	-615	0
582	-618	0
583	-616	0
-583	616	0
583	-619	0
-583	619	0
-645	-581	0
-607	-581	0
-592	-581	0
-646	582	0
-646	-592	0
-646	-607	0
-647	-583	0
-607	-583	0
-592	-583	0
33	-607	0
-33	607	0
33	-608	0
-33	608	0
588	-645	0
-588	645	0
588	-648	0
-588	648	0
589	-646	0
589	-649	0
590	-647	0
-590	647	0
590	-650	0
-590	650	0
-666	-973	0
639	-973	0
666	-974	0
-639	-974	0
-974	588	0
-973	588	0
-640	589	0
-666	-1009	0
641	-1009	0
666	-1010	0
-641	-1010	0
-1010	590	0
-1009	590	0
-123	-108	0
-318	-108	0
-303	-108	0
-333	-108	0
-124	109	0
-319	109	0
-304	109	0
-334	109	0
-125	-110	0
-320	-110	0
-305	-110	0
-335	-110	0
117	-333	0
-117	333	0
117	-336	0
-117	336	0
117	-518	0
-117	518	0
118	-334	0
118	-337	0
118	-519	0
119	-335	0
-119	335	0
119	-338	0
-119	338	0
119	-520	0
-119	520	0
-530	-117	0
-554	-117	0
-534	-117	0
-531	118	0
-531	-534	0
-531	-554	0
-532	-119	0
-554	-119	0
-534	-119	0
29	-554	0
-29	554	0
29	-555	0
-29	555	0
58	-527	0
-58	527	0
58	-530	0
-58	530	0
59	-528	0
59	-531	0
60	-529	0
-60	529	0
60	-532	0
-60	532	0
-67	-983	0
204	-983	0
67	-984	0
-204	-984	0
-984	58	0
-983	58	0
-205	59	0
-67	-1011	0
206	-1011	0
67	-1012	0
-206	-1012	0
-1012	60	0
-1011	60	0
114	-303	0
-114	303	0
114	-306	0
-114	306	0
114	-312	0
-114	312	0
115	-304	0
115	-307	0
115	-313	0
116	-305	0
-116	305	0
116	-308	0
-116	308	0
116	-314	0
-116	314	0
-694	-114	0
-742	-114	0
-698	-114	0
-695	115	0
-695	-698	0
-695	-742	0
-696	-116	0
-742	-116	0
-698	-116	0
31	-742	0
-31	742	0
31	-743	0
-31	743	0
687	-691	0
-687	691	0
687	-694	0
-687	694	0
688	-692	0
688	-695	0
689	-693	0
-689	693	0
689	-696	0
-689	696	0
-837	-965	0
838	-965	0
837	-966	0
-838	-966	0
-966	687	0
-965	687	0
-839	688	0
-837	-1013	0
840	-1013	0
837	-1014	0
-840	-1014	0
-1014	689	0
-1013	689	0
111	-318	0
-111	318	0
111	-321	0
-111	321	0
112	-319	0
112	-322	0
113	-320	0
-113	320	0
113	-323	0
-113	323	0
-842	-111	0
-864	-111	0
-848	-111	0
-843	112	0
-843	-848	0
-843	-864	0
-844	-113	0
-864	-113	0
-848	-113	0
20	-864	0
-20	864	0
20	-865	0
-20	865	0
283	-842	0
-283	842	0
283	-845	0
-283	845	0
284	-843	0
284	-846	0
285	-844	0
-285	844	0
285	-847	0
-285	847	0
-287	-977	0
288	-977	0
287	-978	0
-288	-978	0
-978	283	0
-977	283	0
-289	284	0
-287	-1015	0
290	-1015	0
287	-1016	0
-290	-1016	0
-1016	285	0
-1015	285	0
84	-120	0
-84	120	0
84	-123	0
-84	123	0
85	-121	0
85	-124	0
86	-122	0
-86	122	0
86	-125	0
-86	125	0
-712	-84	0
-768	-84	0
-718	-84	0
-713	85	0
-713	-718	0
-713	-768	0
-714	-86	0
-768	-86	0
-718	-86	0
15	-768	0
-15	768	0
15	-769	0
-15	769	0
703	-712	0
-703	712	0
703	-715	0
-703	715	0
704	-713	0
704	-716	0
705	-714	0
-705	714	0
705	-717	0
-705	717	0
-707	-971	0
708	-971	0
707	-972	0
-708	-972	0
-972	703	0
-971	703	0
-709	704	0
-707	-1017	0
710	-1017	0
707	-1018	0
-710	-1018	0
-1018	705	0
-1017	705	0
-45	-1020	0
43	-1020	0
45	-1021	0
-43	-1021	0
-1021	1019	0
-1020	1019	0
558	43	0
-558	-43	0
-559	44	0
560	45	0
-560	-45	0
247	-558	0
-247	558	0
247	-561	0
-247	561	0
247	-624	0
-247	624	0
248	-559	0
248	-562	0
248	-625	0
249	-560	0
-249	560	0
249	-563	0
-249	563	0
249	-626	0
-249	626	0
577	247	0
-577	-247	0
-578	248	0
579	249	0
-579	-249	0
102	-471	0
-102	471	0
102	-474	0
-102	474	0
102	-577	0
-102	577	0
102	-723	0
-102	723	0
102	-749	0
-102	749	0
102	-871	0
-102	871	0
102	-894	0
-102	894	0
102	-928	0
-102	928	0
103	-472	0
103	-475	0
103	-578	0
103	-724	0
103	-750	0
103	-872	0
103	-895	0
103	-929	0
104	-473	0
-104	473	0
104	-476	0
-104	476	0
104	-579	0
-104	579	0
104	-725	0
-104	725	0
104	-751	0
-104	751	0
104	-873	0
-104	873	0
104	-896	0
-104	896	0
104	-930	0
-104	930	0
75	102	0
105	102	0
90	102	0
-76	103	0
-106	103	0
-91	103	0
77	104	0
107	104	0
92	104	0
-99	-90	0
-94	91	0
-97	91	0
-100	91	0
-101	-92	0
-527	-99	0
-524	-99	0
-516	100	0
-328	100	0
-528	100	0
-528	-524	0
-328	-524	0
-516	-524	0
-529	-101	0
-524	-101	0
564	524	0
537	524	0
535	-564	0
-535	564	0
535	-565	0
-535	565	0
14	535	0
-14	-535	0
330	327	0
-330	-327	0
-331	328	0
332	329	0
-332	-329	0
-336	-330	0
-339	-330	0
-337	331	0
-340	331	0
-338	-332	0
-341	-332	0
518	515	0
521	515	0
-519	516	0
-522	516	0
520	517	0
523	517	0
-845	-96	0
-874	-96	0
-849	-96	0
-846	97	0
-846	-849	0
-846	-874	0
-847	-98	0
-874	-98	0
-849	-98	0
8	-874	0
-8	874	0
8	-875	0
-8	875	0
-322	94	0
-325	94	0
-241	-105	0
-221	-105	0
-244	-105	0
-242	106	0
-222	106	0
-245	106	0
-243	-107	0
-223	-107	0
-246	-107	0
803	244	0
-785	245	0
-810	245	0
-804	245	0
-810	-800	0
-785	-800	0
805	246	0
833	803	0
-671	804	0
-819	804	0
-834	804	0
835	805	0
-955	-833	0
-961	-833	0
-962	-833	0
-956	834	0
-956	-962	0
-956	-961	0
-957	-835	0
-961	-835	0
-962	-835	0
3	-958	0
-3	958	0
3	-961	0
-3	961	0
-821	-818	0
-824	-818	0
-822	819	0
-825	819	0
-823	-820	0
-826	-820	0
-673	-670	0
-676	-670	0
-674	671	0
-677	671	0
-675	-672	0
-678	-672	0
682	673	0
-682	-673	0
-683	674	0
684	675	0
-684	-675	0
904	800	0
909	800	0
908	904	0
-908	-904	0
1	-905	0
-1	905	0
1	-908	0
-1	908	0
-790	-967	0
793	-967	0
790	-968	0
-793	-968	0
-968	784	0
-967	784	0
-791	785	0
-794	785	0
-792	-1023	0
795	-1023	0
792	-1024	0
-795	-1024	0
-1024	786	0
-1023	786	0
-224	-221	0
-230	-221	0
-420	-221	0
-234	-221	0
-225	222	0
-231	222	0
-231	-234	0
-231	-420	0
-225	-234	0
-225	-420	0
-226	-223	0
-232	-223	0
-420	-223	0
-234	-223	0
16	-420	0
-16	420	0
16	-421	0
-16	421	0
-455	-979	0
238	-979	0
455	-980	0
-238	-980	0
-980	224	0
-979	224	0
-456	225	0
-239	225	0
-457	-1025	0
240	-1025	0
457	-1026	0
-240	-1026	0
-1026	226	0
-1025	226	0
274	241	0
-274	-241	0
-275	242	0
276	243	0
-276	-243	0
-280	-274	0
-266	275	0
-278	275	0
-281	275	0
-282	-276	0
-648	-280	0
-631	-280	0
-612	281	0
-643	281	0
-649	281	0
-649	-631	0
-643	-631	0
-612	-631	0
-650	-282	0
-631	-282	0
637	631	0
638	631	0
623	-634	0
-623	634	0
623	-637	0
-623	637	0
13	623	0
-13	-623	0
654	642	0
660	642	0
-655	643	0
-661	643	0
656	644	0
662	644	0
617	611	0
620	611	0
-618	612	0
-621	612	0
619	613	0
622	613	0
-501	-277	0
-507	-277	0
-508	-277	0
-502	278	0
-502	-508	0
-502	-507	0
-503	-279	0
-507	-279	0
-508	-279	0
36	-504	0
-36	504	0
36	-507	0
-36	507	0
-478	266	0
-272	266	0
-69	-75	0
-79	76	0
-82	76	0
-70	76	0
-71	-77	0
72	69	0
-72	-69	0
-73	70	0
74	71	0
-74	-71	0
297	72	0
-292	73	0
-295	73	0
-298	73	0
299	74	0
-691	-297	0
-726	-297	0
-697	-297	0
-692	298	0
-692	-697	0
-692	-726	0
-693	-299	0
-726	-299	0
-697	-299	0
24	-726	0
-24	726	0
24	-727	0
-24	727	0
-312	-294	0
-315	-294	0
-313	295	0
-316	295	0
-314	-296	0
-317	-296	0
300	291	0
-300	-291	0
-301	292	0
302	293	0
-302	-293	0
306	300	0
309	300	0
-307	301	0
-310	301	0
308	302	0
311	302	0
-715	-81	0
-752	-81	0
-719	-81	0
-716	82	0
-716	-719	0
-716	-752	0
-717	-83	0
-752	-83	0
-719	-83	0
2	-752	0
-2	752	0
2	-753	0
-2	753	0
-121	79	0
-236	79	0
-57	-1028	0
55	-1028	0
57	-1029	0
-55	-1029	0
-1029	1027	0
-1028	1027	0
-198	-55	0
-174	-55	0
-199	56	0
-175	56	0
-200	-57	0
-176	-57	0
-189	-174	0
-180	-174	0
-183	-174	0
-375	-174	0
-190	175	0
-181	175	0
-184	175	0
-376	175	0
-191	-176	0
-182	-176	0
-185	-176	0
-377	-176	0
186	-375	0
-186	375	0
186	-378	0
-186	378	0
186	-396	0
-186	396	0
187	-376	0
187	-379	0
187	-397	0
188	-377	0
-188	377	0
188	-380	0
-188	380	0
188	-398	0
-188	398	0
-756	-186	0
-746	-186	0
-750	187	0
-747	187	0
-747	-756	0
-750	753	0
-754	-756	0
-750	-756	0
-756	-188	0
-748	-188	0
759	746	0
-759	-746	0
-760	747	0
761	748	0
-761	-748	0
-763	760	0
-766	760	0
-766	769	0
-763	886	0
571	183	0
574	183	0
-572	184	0
-575	184	0
573	185	0
576	185	0
138	-354	0
-138	354	0
138	-357	0
-138	357	0
138	-363	0
-138	363	0
138	-574	0
-138	574	0
139	-355	0
139	-358	0
139	-364	0
139	-575	0
140	-356	0
-140	356	0
140	-359	0
-140	359	0
140	-365	0
-140	365	0
140	-576	0
-140	576	0
538	138	0
-538	-138	0
-539	139	0
540	140	0
-540	-140	0
-851	-538	0
-855	539	0
-862	539	0
-852	539	0
-862	865	0
-855	858	0
-853	-540	0
868	851	0
-868	-851	0
-869	852	0
870	853	0
-870	-853	0
-878	-868	0
-872	869	0
-872	875	0
-876	-878	0
-872	-878	0
-878	-870	0
348	-366	0
-348	366	0
348	-369	0
-348	369	0
348	-381	0
-348	381	0
348	-402	0
-348	402	0
348	-571	0
-348	571	0
349	-367	0
349	-370	0
349	-382	0
349	-403	0
349	-572	0
350	-368	0
-350	368	0
350	-371	0
-350	371	0
350	-383	0
-350	383	0
350	-404	0
-350	404	0
350	-573	0
-350	573	0
733	348	0
720	348	0
-734	349	0
-721	349	0
735	350	0
722	350	0
-730	-720	0
-724	721	0
-724	727	0
-728	-730	0
-724	-730	0
-730	-722	0
-737	734	0
-740	734	0
-740	743	0
-737	881	0
393	180	0
384	180	0
405	180	0
-394	181	0
-385	181	0
-406	181	0
395	182	0
386	182	0
407	182	0
387	-405	0
-387	405	0
387	-408	0
-387	408	0
388	-406	0
388	-409	0
389	-407	0
-389	407	0
389	-410	0
-389	410	0
414	387	0
-414	-387	0
-415	388	0
416	389	0
-416	-389	0
360	-411	0
-360	411	0
360	-414	0
-360	414	0
361	-412	0
361	-415	0
362	-413	0
-362	413	0
362	-416	0
-362	416	0
-594	-360	0
-598	361	0
-605	361	0
-595	361	0
-605	608	0
-598	601	0
-596	-362	0
628	594	0
-625	595	0
-625	-634	0
-635	628	0
-625	628	0
628	596	0
-433	-384	0
-428	385	0
-418	385	0
-434	385	0
-435	-386	0
253	-430	0
-253	430	0
253	-433	0
-253	433	0
254	-431	0
254	-434	0
255	-432	0
-255	432	0
255	-435	0
-255	435	0
-256	-253	0
-260	254	0
-263	254	0
-257	254	0
-263	486	0
-260	509	0
-258	-255	0
467	256	0
-467	-256	0
-468	257	0
469	258	0
-469	-258	0
-490	-467	0
-475	468	0
-475	504	0
-505	-490	0
-475	-490	0
-490	-469	0
-424	-417	0
-472	418	0
-472	421	0
-422	-424	0
-472	-424	0
-424	-419	0
-437	428	0
-440	428	0
-440	443	0
-437	772	0
345	-390	0
-345	390	0
345	-393	0
-345	393	0
346	-391	0
346	-394	0
347	-392	0
-347	392	0
347	-395	0
-347	395	0
568	345	0
541	345	0
-562	346	0
-542	346	0
-542	568	0
-562	-565	0
-566	568	0
-562	568	0
568	347	0
543	347	0
-545	542	0
-552	542	0
-552	555	0
-545	548	0
177	-189	0
-177	189	0
177	-192	0
-177	192	0
178	-190	0
178	-193	0
179	-191	0
-179	191	0
179	-194	0
-179	194	0
-812	-177	0
-828	178	0
-831	178	0
-813	178	0
-831	934	0
-828	942	0
-814	-179	0
815	812	0
-815	-812	0
-816	813	0
817	814	0
-817	-814	0
-938	-815	0
-929	816	0
-929	958	0
-959	-938	0
-929	-938	0
-938	-817	0
-911	-198	0
-918	-198	0
-915	199	0
-912	199	0
-912	-918	0
-915	921	0
-915	-918	0
-922	-918	0
-913	-200	0
-918	-200	0
891	911	0
-891	-911	0
-892	912	0
893	913	0
-893	-913	0
-895	892	0
-902	892	0
-902	898	0
-895	905	0
-51	-1031	0
49	-1031	0
51	-1032	0
-49	-1032	0
-1032	1030	0
-1031	1030	0
150	49	0
159	49	0
132	49	0
144	49	0
-151	50	0
-160	50	0
-133	50	0
-145	50	0
152	51	0
161	51	0
134	51	0
146	51	0
135	-144	0
-135	144	0
135	-147	0
-135	147	0
135	-351	0
-135	351	0
135	-399	0
-135	399	0
136	-145	0
136	-148	0
136	-352	0
136	-400	0
137	-146	0
-137	146	0
137	-149	0
-137	149	0
137	-353	0
-137	353	0
137	-401	0
-137	401	0
396	135	0
-396	-135	0
-397	136	0
398	137	0
-398	-137	0
363	132	0
411	132	0
369	132	0
-364	133	0
-412	133	0
-370	133	0
365	134	0
413	134	0
371	134	0
129	-159	0
-129	159	0
129	-162	0
-129	162	0
130	-160	0
130	-163	0
131	-161	0
-131	161	0
131	-164	0
-131	164	0
351	129	0
357	129	0
366	129	0
342	129	0
-352	130	0
-358	130	0
-367	130	0
-343	130	0
353	131	0
359	131	0
368	131	0
344	131	0
390	342	0
-390	-342	0
-391	343	0
392	344	0
-392	-344	0
126	-150	0
-126	150	0
126	-153	0
-126	153	0
126	-171	0
-126	171	0
127	-151	0
127	-154	0
127	-172	0
128	-152	0
-128	152	0
128	-155	0
-128	155	0
128	-173	0
-128	173	0
192	126	0
-192	-126	0
-193	127	0
194	128	0
-194	-128	0
-48	-1034	0
46	-1034	0
48	-1035	0
-46	-1035	0
-1035	1033	0
-1034	1033	0
354	46	0
165	46	0
147	46	0
153	46	0
-355	47	0
-166	47	0
-148	47	0
-154	47	0
356	48	0
167	48	0
149	48	0
155	48	0
141	-165	0
-141	165	0
141	-168	0
-141	168	0
142	-166	0
142	-169	0
143	-167	0
-143	167	0
143	-170	0
-143	170	0
372	141	0
-372	-141	0
-373	142	0
374	143	0
-374	-143	0
-378	-372	0
-381	-372	0
-379	373	0
-382	373	0
-380	-374	0
-383	-374	0
-54	-1037	0
52	-1037	0
54	-1038	0
-52	-1038	0
-1038	1036	0
-1037	1036	0
162	52	0
168	52	0
156	52	0
171	52	0
-163	53	0
-169	53	0
-157	53	0
-172	53	0
164	54	0
170	54	0
158	54	0
173	54	0
399	156	0
430	156	0
402	156	0
408	156	0
-400	157	0
-431	157	0
-403	157	0
-409	157	0
401	158	0
432	158	0
404	158	0
410	158	0
-1036	1039	0
-1033	1039	0
-1030	1039	0
-1027	1039	0
-1019	1039	0
-994	1039	0
-987	1039	0
-986	41	38	0
988	39	-37	0
989	-39	37	0
-987	989	988	0
-38	37	39	0
-38	-37	-39	0
-202	201	203	0
-202	-201	-203	0
-950	949	951	0
-950	-949	-951	0
-915	914	916	0
-915	-914	-916	0
-855	854	856	0
-855	-854	-856	0
-839	838	840	0
-839	-838	-840	0
-828	827	829	0
-828	-827	-829	0
-779	778	780	0
-779	-778	-780	0
-763	762	764	0
-763	-762	-764	0
-737	736	738	0
-737	-736	-738	0
-709	708	710	0
-709	-708	-710	0
-640	639	641	0
-640	-639	-641	0
-598	597	599	0
-598	-597	-599	0
-545	544	546	0
-545	-544	-546	0
-496	495	497	0
-496	-495	-497	0
-437	436	438	0
-437	-436	-438	0
-289	288	290	0
-289	-288	-290	0
-260	259	261	0
-260	-259	-261	0
-215	214	216	0
-215	-214	-216	0
-208	207	209	0
-208	-207	-209	0
-205	204	206	0
-205	-204	-206	0
-63	62	64	0
-63	-62	-64	0
686	884	885	0
65	286	68	0
61	547	533	0
66	857	850	0
494	512	513	0
926	945	946	0
777	924	925	0
213	775	776	0
591	600	593	0
702	889	890	0
995	42	-40	0
996	-42	40	0
-994	996	995	0
-41	40	42	0
-41	-40	-42	0
-677	676	678	0
-677	-676	-678	0
-661	660	662	0
-661	-660	-662	0
-658	657	659	0
-658	-657	-659	0
-196	195	197	0
-196	-195	-197	0
-902	901	903	0
-902	-901	-903	0
-862	861	863	0
-862	-861	-863	0
-831	830	832	0
-831	-830	-832	0
-825	824	826	0
-825	-824	-826	0
-794	793	795	0
-794	-793	-795	0
-766	765	767	0
-766	-765	-767	0
-740	739	741	0
-740	-739	-741	0
-621	620	622	0
-621	-620	-622	0
-605	604	606	0
-605	-604	-606	0
-552	551	553	0
-552	-551	-553	0
-522	521	523	0
-522	-521	-523	0
-440	439	441	0
-440	-439	-441	0
-340	339	341	0
-340	-339	-341	0
-325	324	326	0
-325	-324	-326	0
-316	315	317	0
-316	-315	-317	0
-310	309	311	0
-310	-309	-311	0
-272	271	273	0
-272	-271	-273	0
-263	262	264	0
-263	-262	-264	0
-251	250	252	0
-251	-250	-252	0
-239	238	240	0
-239	-238	-240	0
-236	235	237	0
-236	-235	-237	0
-465	-466	448	0
-465	-464	446	0
-465	446	448	0
-465	-466	653	0
-465	-464	651	0
-465	651	653	0
-465	-466	110	0
-465	-464	108	0
-465	108	110	0
-447	-448	466	0
-447	-446	464	0
-447	464	466	0
-447	-448	653	0
-447	-446	651	0
-447	651	653	0
-447	-448	110	0
-447	-446	108	0
-447	108	110	0
-652	-653	466	0
-652	-651	464	0
-652	464	466	0
-652	-653	448	0
-652	-651	446	0
-652	446	448	0
-652	-653	110	0
-652	-651	108	0
-652	108	110	0
-109	-110	466	0
-109	-108	464	0
-109	464	466	0
-109	-110	448	0
-109	-108	446	0
-109	446	448	0
-109	-110	653	0
-109	-108	651	0
-109	651	653	0
-88	87	89	0
-88	-87	-89	0
-465	464	466	0
-465	-464	-466	0
-269	478	481	0
-481	480	482	0
-481	-480	-482	0
-478	477	479	0
-478	-477	-479	0
-269	268	270	0
-269	-268	-270	0
-484	499	502	0
-502	501	503	0
-502	-501	-503	0
-499	498	500	0
-499	-498	-500	0
975	668	-495	0
976	-668	495	0
-483	976	975	0
-484	483	485	0
-484	-483	-485	0
1001	668	-497	0
1002	-668	497	0
-485	1002	1001	0
-680	-681	-787	0
-680	-679	-789	0
-680	-787	-789	0
-680	-681	-458	0
-680	-679	-460	0
-680	-458	-460	0
-788	-789	-679	0
-788	-787	-681	0
-788	-679	-681	0
-788	-789	-458	0
-788	-787	-460	0
-788	-458	-460	0
-459	-460	-679	0
-459	-458	-681	0
-459	-679	-681	0
-459	-460	-787	0
-459	-458	-789	0
-459	-787	-789	0
-447	446	448	0
-447	-446	-448	0
-822	821	823	0
-822	-821	-823	0
-683	682	684	0
-683	-682	-684	0
-680	679	681	0
-680	-679	-681	0
-453	452	454	0
-453	-452	-454	0
-932	953	956	0
-956	955	957	0
-956	-955	-957	0
-953	952	954	0
-953	-952	-954	0
963	948	-949	0
964	-948	949	0
-931	964	963	0
-932	931	933	0
-932	-931	-933	0
1003	948	-951	0
1004	-948	951	0
-933	1004	1003	0
-450	788	791	0
-791	790	792	0
-791	-790	-792	0
-788	787	789	0
-788	-787	-789	0
-450	449	451	0
-450	-449	-451	0
-585	807	810	0
-810	809	811	0
-810	-809	-811	0
-807	806	808	0
-807	-806	-808	0
969	782	-778	0
970	-782	778	0
-584	970	969	0
-585	584	586	0
-585	-584	-586	0
1005	782	-780	0
1006	-782	780	0
-586	1006	1005	0
-218	456	459	0
-459	458	460	0
-459	-458	-460	0
-456	455	457	0
-456	-455	-457	0
-218	217	219	0
-218	-217	-219	0
-211	228	231	0
-231	230	232	0
-231	-230	-232	0
-228	227	229	0
-228	-227	-229	0
981	798	-214	0
982	-798	214	0
-210	982	981	0
-211	210	212	0
-211	-210	-212	0
1007	798	-216	0
1008	-798	216	0
-212	1008	1007	0
-462	652	655	0
-655	654	656	0
-655	-654	-656	0
-652	651	653	0
-652	-651	-653	0
-462	461	463	0
-462	-461	-463	0
-582	615	618	0
-618	617	619	0
-618	-617	-619	0
-615	614	616	0
-615	-614	-616	0
-582	581	583	0
-582	-581	-583	0
-589	646	649	0
-649	648	650	0
-649	-648	-650	0
-646	645	647	0
-646	-645	-647	0
973	666	-639	0
974	-666	639	0
-588	974	973	0
-589	588	590	0
-589	-588	-590	0
1009	666	-641	0
1010	-666	641	0
-590	1010	1009	0
-334	-335	-303	0
-334	-333	-305	0
-334	-303	-305	0
-334	-335	-318	0
-334	-333	-320	0
-334	-318	-320	0
-334	-335	-123	0
-334	-333	-125	0
-334	-123	-125	0
-304	-305	-333	0
-304	-303	-335	0
-304	-333	-335	0
-304	-305	-318	0
-304	-303	-320	0
-304	-318	-320	0
-304	-305	-123	0
-304	-303	-125	0
-304	-123	-125	0
-319	-320	-333	0
-319	-318	-335	0
-319	-333	-335	0
-319	-320	-303	0
-319	-318	-305	0
-319	-303	-305	0
-319	-320	-123	0
-319	-318	-125	0
-319	-123	-125	0
-124	-125	-333	0
-124	-123	-335	0
-124	-333	-335	0
-124	-125	-303	0
-124	-123	-305	0
-124	-303	-305	0
-124	-125	-318	0
-124	-123	-320	0
-124	-318	-320	0
-109	108	110	0
-109	-108	-110	0
-519	518	520	0
-519	-518	-520	0
-337	336	338	0
-337	-336	-338	0
-334	333	335	0
-334	-333	-335	0
-118	117	119	0
-118	-117	-119	0
-59	528	531	0
-531	530	532	0
-531	-530	-532	0
-528	527	529	0
-528	-527	-529	0
983	67	-204	0
984	-67	204	0
-58	984	983	0
-59	58	60	0
-59	-58	-60	0
1011	67	-206	0
1012	-67	206	0
-60	1012	1011	0
-313	312	314	0
-313	-312	-314	0
-307	306	308	0
-307	-306	-308	0
-304	303	305	0
-304	-303	-305	0
-115	114	116	0
-115	-114	-116	0
-688	692	695	0
-695	694	696	0
-695	-694	-696	0
-692	691	693	0
-692	-691	-693	0
965	837	-838	0
966	-837	838	0
-687	966	965	0
-688	687	689	0
-688	-687	-689	0
1013	837	-840	0
1014	-837	840	0
-689	1014	1013	0
-112	319	322	0
-322	321	323	0
-322	-321	-323	0
-319	318	320	0
-319	-318	-320	0
-112	111	113	0
-112	-111	-113	0
-284	843	846	0
-846	845	847	0
-846	-845	-847	0
-843	842	844	0
-843	-842	-844	0
977	287	-288	0
978	-287	288	0
-283	978	977	0
-284	283	285	0
-284	-283	-285	0
1015	287	-290	0
1016	-287	290	0
-285	1016	1015	0
-85	121	124	0
-124	123	125	0
-124	-123	-125	0
-121	120	122	0
-121	-120	-122	0
-85	84	86	0
-85	-84	-86	0
-704	713	716	0
-716	715	717	0
-716	-715	-717	0
-713	712	714	0
-713	-712	-714	0
971	707	-708	0
972	-707	708	0
-703	972	971	0
-704	703	705	0
-704	-703	-705	0
1017	707	-710	0
1018	-707	710	0
-705	1018	1017	0
1020	45	-43	0
1021	-45	43	0
-1019	1021	1020	0
-44	43	45	0
-44	-43	-45	0
-625	624	626	0
-625	-624	-626	0
-562	561	563	0
-562	-561	-563	0
-559	558	560	0
-559	-558	-560	0
-248	247	249	0
-248	-247	-249	0
-929	928	930	0
-929	-928	-930	0
-895	894	896	0
-895	-894	-896	0
-872	871	873	0
-872	-871	-873	0
-750	749	751	0
-750	-749	-751	0
-724	723	725	0
-724	-723	-725	0
-578	577	579	0
-578	-577	-579	0
-475	474	476	0
-475	-474	-476	0
-472	471	473	0
-472	-471	-473	0
-91	-92	107	0
-91	-90	105	0
-91	105	107	0
-91	-92	77	0
-91	-90	75	0
-91	75	77	0
-106	-107	92	0
-106	-105	90	0
-106	90	92	0
-106	-107	77	0
-106	-105	75	0
-106	75	77	0
-76	-77	92	0
-76	-75	90	0
-76	90	92	0
-76	-77	107	0
-76	-75	105	0
-76	105	107	0
-103	102	104	0
-103	-102	-104	0
-96	-93	-90	0
99	93	90	0
99	96	90	0
-97	-98	95	0
-97	-96	93	0
-97	93	95	0
-94	-95	98	0
-94	-93	96	0
-94	96	98	0
-97	-98	-99	0
-97	-96	-101	0
-97	-99	-101	0
-94	-95	-99	0
-94	-93	-101	0
-94	-99	-101	0
-91	90	92	0
-91	-90	-92	0
-98	-95	-92	0
101	95	92	0
101	98	92	0
-327	-515	-99	0
-525	-526	-527	0
-525	-524	-529	0
-525	-527	-529	0
-328	-329	517	0
-328	-327	515	0
-328	515	517	0
-516	-517	329	0
-516	-515	327	0
-516	327	329	0
-328	-329	-527	0
-328	-327	-529	0
-328	-527	-529	0
-516	-517	-527	0
-516	-515	-529	0
-516	-527	-529	0
-100	99	101	0
-100	-99	-101	0
-329	-517	-101	0
-524	-564	-537	0
-328	327	329	0
-328	-327	-329	0
330	336	339	0
-340	-341	-336	0
-340	-339	-338	0
-340	-336	-338	0
-337	-338	-339	0
-337	-336	-341	0
-337	-339	-341	0
-331	330	332	0
-331	-330	-332	0
332	338	341	0
-515	-518	-521	0
-522	-523	520	0
-522	-521	518	0
-522	518	520	0
-519	-520	523	0
-519	-518	521	0
-519	521	523	0
-516	515	517	0
-516	-515	-517	0
-517	-520	-523	0
-97	96	98	0
-97	-96	-98	0
324	321	93	0
-324	-321	93	0
-324	321	-93	0
324	-321	-93	0
-94	93	95	0
-94	-93	-95	0
326	323	95	0
-326	-323	95	0
-326	323	-95	0
326	-323	-95	0
-245	-246	-221	0
-245	-244	-223	0
-245	-221	-223	0
-245	-246	-241	0
-245	-244	-243	0
-245	-241	-243	0
-222	-223	-244	0
-222	-221	-246	0
-222	-244	-246	0
-222	-223	-241	0
-222	-221	-243	0
-222	-241	-243	0
-242	-243	-244	0
-242	-241	-246	0
-242	-244	-246	0
-242	-243	-221	0
-242	-241	-223	0
-242	-221	-223	0
-106	105	107	0
-106	-105	-107	0
-803	-784	-244	0
-803	-809	-244	0
-803	-800	-244	0
-801	-802	-809	0
-801	-800	-811	0
-801	-809	-811	0
-801	-802	-784	0
-801	-800	-786	0
-801	-784	-786	0
-810	-811	-784	0
-810	-809	-786	0
-810	-784	-786	0
-785	-786	-809	0
-785	-784	-811	0
-785	-809	-811	0
-801	-802	805	0
-801	-800	803	0
-801	803	805	0
-810	-811	805	0
-810	-809	803	0
-810	803	805	0
-785	-786	805	0
-785	-784	803	0
-785	803	805	0
-245	244	246	0
-245	-244	-246	0
-805	-786	-246	0
-805	-811	-246	0
-805	-800	-246	0
818	670	803	0
-833	-670	-803	0
-833	-818	-803	0
-819	-820	-670	0
-819	-818	-672	0
-819	-670	-672	0
-671	-672	-818	0
-671	-670	-820	0
-671	-818	-820	0
-819	-820	835	0
-819	-818	833	0
-819	833	835	0
-671	-672	835	0
-671	-670	833	0
-671	833	835	0
-804	803	805	0
-804	-803	-805	0
820	672	805	0
-835	-672	-805	0
-835	-820	-805	0
-834	833	835	0
-834	-833	-835	0
818	821	824	0
-825	-826	-821	0
-825	-824	-823	0
-825	-821	-823	0
-822	-823	-824	0
-822	-821	-826	0
-822	-824	-826	0
-819	818	820	0
-819	-818	-820	0
820	823	826	0
670	673	676	0
-677	-678	-673	0
-677	-676	-675	0
-677	-673	-675	0
-674	-675	-676	0
-674	-673	-678	0
-674	-676	-678	0
-671	670	672	0
-671	-670	-672	0
672	675	678	0
-674	673	675	0
-674	-673	-675	0
-800	-904	-909	0
967	790	-793	0
968	-790	793	0
-784	968	967	0
-785	784	786	0
-785	-784	-786	0
1023	792	-795	0
1024	-792	795	0
-786	1024	1023	0
-231	-232	-224	0
-231	-230	-226	0
-231	-224	-226	0
-225	-226	-230	0
-225	-224	-232	0
-225	-230	-232	0
-222	221	223	0
-222	-221	-223	0
979	455	-238	0
980	-455	238	0
-224	980	979	0
-225	224	226	0
-225	-224	-226	0
1025	457	-240	0
1026	-457	240	0
-226	1026	1025	0
-242	241	243	0
-242	-241	-243	0
-277	-265	-274	0
280	265	274	0
280	277	274	0
-278	-279	267	0
-278	-277	265	0
-278	265	267	0
-266	-267	279	0
-266	-265	277	0
-266	277	279	0
-278	-279	-280	0
-278	-277	-282	0
-278	-280	-282	0
-266	-267	-280	0
-266	-265	-282	0
-266	-280	-282	0
-275	274	276	0
-275	-274	-276	0
-279	-267	-276	0
282	267	276	0
282	279	276	0
-642	-611	-280	0
-632	-633	-648	0
-632	-631	-650	0
-632	-648	-650	0
-643	-644	613	0
-643	-642	611	0
-643	611	613	0
-612	-613	644	0
-612	-611	642	0
-612	642	644	0
-643	-644	-648	0
-643	-642	-650	0
-643	-648	-650	0
-612	-613	-648	0
-612	-611	-650	0
-612	-648	-650	0
-281	280	282	0
-281	-280	-282	0
-644	-613	-282	0
-631	-637	-638	0
-642	-654	-660	0
-661	-662	656	0
-661	-660	654	0
-661	654	656	0
-655	-656	662	0
-655	-654	660	0
-655	660	662	0
-643	642	644	0
-643	-642	-644	0
-644	-656	-662	0
-611	-617	-620	0
-621	-622	619	0
-621	-620	617	0
-621	617	619	0
-618	-619	622	0
-618	-617	620	0
-618	620	622	0
-612	611	613	0
-612	-611	-613	0
-613	-619	-622	0
-278	277	279	0
-278	-277	-279	0
271	477	265	0
-271	-477	265	0
-271	477	-265	0
271	-477	-265	0
-266	265	267	0
-266	-265	-267	0
273	479	267	0
-273	-479	267	0
-273	479	-267	0
273	-479	-267	0
-81	-78	-75	0
69	78	75	0
69	81	75	0
-82	-83	80	0
-82	-81	78	0
-82	78	80	0
-79	-80	83	0
-79	-78	81	0
-79	81	83	0
-82	-83	-69	0
-82	-81	-71	0
-82	-69	-71	0
-79	-80	-69	0
-79	-78	-71	0
-79	-69	-71	0
-76	75	77	0
-76	-75	-77	0
-83	-80	-77	0
71	80	77	0
71	83	77	0
-70	69	71	0
-70	-69	-71	0
294	291	72	0
-297	-291	-72	0
-297	-294	-72	0
-295	-296	-291	0
-295	-294	-293	0
-295	-291	-293	0
-292	-293	-294	0
-292	-291	-296	0
-292	-294	-296	0
-295	-296	299	0
-295	-294	297	0
-295	297	299	0
-292	-293	299	0
-292	-291	297	0
-292	297	299	0
-73	72	74	0
-73	-72	-74	0
296	293	74	0
-299	-293	-74	0
-299	-296	-74	0
-298	297	299	0
-298	-297	-299	0
294	312	315	0
-316	-317	-312	0
-316	-315	-314	0
-316	-312	-314	0
-313	-314	-315	0
-313	-312	-317	0
-313	-315	-317	0
-295	294	296	0
-295	-294	-296	0
296	314	317	0
-292	291	293	0
-292	-291	-293	0
-300	-306	-309	0
-310	-311	308	0
-310	-309	306	0
-310	306	308	0
-307	-308	311	0
-307	-306	309	0
-307	309	311	0
-301	300	302	0
-301	-300	-302	0
-302	-308	-311	0
-82	81	83	0
-82	-81	-83	0
235	120	78	0
-235	-120	78	0
-235	120	-78	0
235	-120	-78	0
-79	78	80	0
-79	-78	-80	0
237	122	80	0
-237	-122	80	0
-237	122	-80	0
237	-122	-80	0
1028	57	-55	0
1029	-57	55	0
-1027	1029	1028	0
55	198	174	0
-175	-176	-198	0
-175	-174	-200	0
-175	-198	-200	0
-199	-200	-174	0
-199	-198	-176	0
-199	-174	-176	0
-56	55	57	0
-56	-55	-57	0
57	200	176	0
-376	-377	-183	0
-376	-375	-185	0
-376	-183	-185	0
-376	-377	-180	0
-376	-375	-182	0
-376	-180	-182	0
-376	-377	-189	0
-376	-375	-191	0
-376	-189	-191	0
-184	-185	-375	0
-184	-183	-377	0
-184	-375	-377	0
-184	-185	-180	0
-184	-183	-182	0
-184	-180	-182	0
-184	-185	-189	0
-184	-183	-191	0
-184	-189	-191	0
-181	-182	-375	0
-181	-180	-377	0
-181	-375	-377	0
-181	-182	-183	0
-181	-180	-185	0
-181	-183	-185	0
-181	-182	-189	0
-181	-180	-191	0
-181	-189	-191	0
-190	-191	-375	0
-190	-189	-377	0
-190	-375	-377	0
-190	-191	-183	0
-190	-189	-185	0
-190	-183	-185	0
-190	-191	-180	0
-190	-189	-182	0
-190	-180	-182	0
-175	174	176	0
-175	-174	-176	0
-397	396	398	0
-397	-396	-398	0
-379	378	380	0
-379	-378	-380	0
-376	375	377	0
-376	-375	-377	0
-753	-749	-186	0
-757	-758	-746	0
-757	-756	-748	0
-757	-746	-748	0
-754	-755	751	0
-754	-753	749	0
-754	749	751	0
-754	-755	-746	0
-754	-753	-748	0
-754	-746	-748	0
-750	-751	-746	0
-750	-749	-748	0
-750	-746	-748	0
-187	186	188	0
-187	-186	-188	0
-753	-751	-188	0
-747	746	748	0
-747	-746	-748	0
-886	-762	-759	0
-769	-765	-759	0
765	762	759	0
769	762	759	0
765	886	759	0
769	886	759	0
-770	-771	767	0
-770	-769	765	0
-770	765	767	0
-887	-888	764	0
-887	-886	762	0
-887	762	764	0
-760	759	761	0
-760	-759	-761	0
-886	-764	-761	0
-769	-767	-761	0
767	764	761	0
769	764	761	0
767	886	761	0
769	886	761	0
-183	-571	-574	0
-575	-576	573	0
-575	-574	571	0
-575	571	573	0
-572	-573	576	0
-572	-571	574	0
-572	574	576	0
-184	183	185	0
-184	-183	-185	0
-185	-573	-576	0
-575	574	576	0
-575	-574	-576	0
-364	363	365	0
-364	-363	-365	0
-358	357	359	0
-358	-357	-359	0
-355	354	356	0
-355	-354	-356	0
-139	138	140	0
-139	-138	-140	0
-858	-854	-538	0
-865	-861	-538	0
-866	-867	863	0
-866	-865	861	0
-866	861	863	0
-859	-860	856	0
-859	-858	854	0
-859	854	856	0
-866	-867	-851	0
-866	-865	-853	0
-866	-851	-853	0
-862	-863	-851	0
-862	-861	-853	0
-862	-851	-853	0
-859	-860	-851	0
-859	-858	-853	0
-859	-851	-853	0
-855	-856	-851	0
-855	-854	-853	0
-855	-851	-853	0
-539	538	540	0
-539	-538	-540	0
-858	-856	-540	0
-865	-863	-540	0
-852	851	853	0
-852	-851	-853	0
-875	-871	-868	0
878	871	868	0
878	875	868	0
-876	-877	873	0
-876	-875	871	0
-876	871	873	0
-869	868	870	0
-869	-868	-870	0
-875	-873	-870	0
878	873	870	0
878	875	870	0
-572	571	573	0
-572	-571	-573	0
-403	402	404	0
-403	-402	-404	0
-382	381	383	0
-382	-381	-383	0
-370	369	371	0
-370	-369	-371	0
-367	366	368	0
-367	-366	-368	0
-348	-733	-720	0
-721	-722	735	0
-721	-720	733	0
-721	733	735	0
-734	-735	722	0
-734	-733	720	0
-734	720	722	0
-349	348	350	0
-349	-348	-350	0
-350	-735	-722	0
-727	-723	-720	0
730	723	720	0
730	727	720	0
-728	-729	725	0
-728	-727	723	0
-728	723	725	0
-721	720	722	0
-721	-720	-722	0
-727	-725	-722	0
730	725	722	0
730	727	722	0
-881	-736	-733	0
-743	-739	-733	0
739	736	733	0
743	736	733	0
739	881	733	0
743	881	733	0
-744	-745	741	0
-744	-743	739	0
-744	739	741	0
-882	-883	738	0
-882	-881	736	0
-882	736	738	0
-734	733	735	0
-734	-733	-735	0
-881	-738	-735	0
-743	-741	-735	0
741	738	735	0
743	738	735	0
741	881	735	0
743	881	735	0
-406	-407	386	0
-406	-405	384	0
-406	384	386	0
-406	-407	395	0
-406	-405	393	0
-406	393	395	0
-385	-386	407	0
-385	-384	405	0
-385	405	407	0
-385	-386	395	0
-385	-384	393	0
-385	393	395	0
-394	-395	407	0
-394	-393	405	0
-394	405	407	0
-394	-395	386	0
-394	-393	384	0
-394	384	386	0
-181	180	182	0
-181	-180	-182	0
-388	406	409	0
-409	408	410	0
-409	-408	-410	0
-406	405	407	0
-406	-405	-407	0
-388	387	389	0
-388	-387	-389	0
-361	412	415	0
-415	414	416	0
-415	-414	-416	0
-412	411	413	0
-412	-411	-413	0
-601	-597	-360	0
-608	-604	-360	0
-609	-610	606	0
-609	-608	604	0
-609	604	606	0
-602	-603	599	0
-602	-601	597	0
-602	597	599	0
-609	-610	-594	0
-609	-608	-596	0
-609	-594	-596	0
-605	-606	-594	0
-605	-604	-596	0
-605	-594	-596	0
-602	-603	-594	0
-602	-601	-596	0
-602	-594	-596	0
-598	-599	-594	0
-598	-597	-596	0
-598	-594	-596	0
-361	360	362	0
-361	-360	-362	0
-601	-599	-362	0
-608	-606	-362	0
634	624	594	0
-628	-624	-594	0
-628	-634	-594	0
-635	-636	-624	0
-635	-634	-626	0
-635	-624	-626	0
-595	594	596	0
-595	-594	-596	0
634	626	596	0
-628	-626	-596	0
-628	-634	-596	0
-417	-427	-384	0
433	427	384	0
433	417	384	0
-418	-419	429	0
-418	-417	427	0
-418	427	429	0
-428	-429	419	0
-428	-427	417	0
-428	417	419	0
-418	-419	-433	0
-418	-417	-435	0
-418	-433	-435	0
-428	-429	-433	0
-428	-427	-435	0
-428	-433	-435	0
-385	384	386	0
-385	-384	-386	0
-419	-429	-386	0
435	429	386	0
435	419	386	0
-254	431	434	0
-434	433	435	0
-434	-433	-435	0
-431	430	432	0
-431	-430	-432	0
-509	-259	-253	0
-486	-262	-253	0
-487	-488	264	0
-487	-486	262	0
-487	262	264	0
-510	-511	261	0
-510	-509	259	0
-510	259	261	0
-487	-488	-256	0
-487	-486	-258	0
-487	-256	-258	0
-263	-264	-256	0
-263	-262	-258	0
-263	-256	-258	0
-510	-511	-256	0
-510	-509	-258	0
-510	-256	-258	0
-260	-261	-256	0
-260	-259	-258	0
-260	-256	-258	0
-254	253	255	0
-254	-253	-255	0
-509	-261	-255	0
-486	-264	-255	0
-257	256	258	0
-257	-256	-258	0
-504	-474	-467	0
490	474	467	0
490	504	467	0
-505	-506	476	0
-505	-504	474	0
-505	474	476	0
-468	467	469	0
-468	-467	-469	0
-504	-476	-469	0
490	476	469	0
490	504	469	0
-421	-471	-417	0
424	471	417	0
424	421	417	0
-422	-423	473	0
-422	-421	471	0
-422	471	473	0
-418	417	419	0
-418	-417	-419	0
-421	-473	-419	0
424	473	419	0
424	421	419	0
-772	-436	-427	0
-443	-439	-427	0
439	436	427	0
443	436	427	0
439	772	427	0
443	772	427	0
-444	-445	441	0
-444	-443	439	0
-444	439	441	0
-773	-774	438	0
-773	-772	436	0
-773	436	438	0
-428	427	429	0
-428	-427	-429	0
-772	-438	-429	0
-443	-441	-429	0
441	438	429	0
443	438	429	0
441	772	429	0
443	772	429	0
-346	391	394	0
-394	393	395	0
-394	-393	-395	0
-391	390	392	0
-391	-390	-392	0
565	561	345	0
-569	-570	543	0
-569	-568	541	0
-569	541	543	0
-566	-567	-561	0
-566	-565	-563	0
-566	-561	-563	0
-566	-567	543	0
-566	-565	541	0
-566	541	543	0
-562	-563	543	0
-562	-561	541	0
-562	541	543	0
-346	345	347	0
-346	-345	-347	0
565	563	347	0
-548	-544	-541	0
-555	-551	-541	0
551	544	541	0
555	544	541	0
551	548	541	0
555	548	541	0
-556	-557	553	0
-556	-555	551	0
-556	551	553	0
-549	-550	546	0
-549	-548	544	0
-549	544	546	0
-542	541	543	0
-542	-541	-543	0
-548	-546	-543	0
-555	-553	-543	0
553	546	543	0
555	546	543	0
553	548	543	0
555	548	543	0
-178	190	193	0
-193	192	194	0
-193	-192	-194	0
-190	189	191	0
-190	-189	-191	0
-942	-827	-177	0
-934	-830	-177	0
-935	-936	832	0
-935	-934	830	0
-935	830	832	0
-943	-944	829	0
-943	-942	827	0
-943	827	829	0
-935	-936	-812	0
-935	-934	-814	0
-935	-812	-814	0
-831	-832	-812	0
-831	-830	-814	0
-831	-812	-814	0
-943	-944	-812	0
-943	-942	-814	0
-943	-812	-814	0
-828	-829	-812	0
-828	-827	-814	0
-828	-812	-814	0
-178	177	179	0
-178	-177	-179	0
-942	-829	-179	0
-934	-832	-179	0
-813	812	814	0
-813	-812	-814	0
-958	-928	-815	0
938	928	815	0
938	958	815	0
-959	-960	930	0
-959	-958	928	0
-959	928	930	0
-816	815	817	0
-816	-815	-817	0
-958	-930	-817	0
938	930	817	0
938	958	817	0
-914	-921	-198	0
-919	-920	-911	0
-919	-918	-913	0
-919	-911	-913	0
-922	-923	916	0
-922	-921	914	0
-922	914	916	0
-915	-916	-911	0
-915	-914	-913	0
-915	-911	-913	0
-922	-923	-911	0
-922	-921	-913	0
-922	-911	-913	0
-199	198	200	0
-199	-198	-200	0
-916	-921	-200	0
-912	911	913	0
-912	-911	-913	0
-894	-905	-891	0
-901	-898	-891	0
898	905	891	0
901	905	891	0
898	894	891	0
901	894	891	0
-899	-900	903	0
-899	-898	901	0
-899	901	903	0
-906	-907	896	0
-906	-905	894	0
-906	894	896	0
-892	891	893	0
-892	-891	-893	0
-896	-905	-893	0
-903	-898	-893	0
898	905	893	0
903	905	893	0
898	896	893	0
903	896	893	0
1031	51	-49	0
1032	-51	49	0
-1030	1032	1031	0
-145	-146	134	0
-145	-144	132	0
-145	132	134	0
-145	-146	161	0
-145	-144	159	0
-145	159	161	0
-145	-146	152	0
-145	-144	150	0
-145	150	152	0
-133	-134	146	0
-133	-132	144	0
-133	144	146	0
-133	-134	161	0
-133	-132	159	0
-133	159	161	0
-133	-134	152	0
-133	-132	150	0
-133	150	152	0
-160	-161	146	0
-160	-159	144	0
-160	144	146	0
-160	-161	134	0
-160	-159	132	0
-160	132	134	0
-160	-161	152	0
-160	-159	150	0
-160	150	152	0
-151	-152	146	0
-151	-150	144	0
-151	144	146	0
-151	-152	134	0
-151	-150	132	0
-151	132	134	0
-151	-152	161	0
-151	-150	159	0
-151	159	161	0
-50	49	51	0
-50	-49	-51	0
-400	399	401	0
-400	-399	-401	0
-352	351	353	0
-352	-351	-353	0
-148	147	149	0
-148	-147	-149	0
-145	144	146	0
-145	-144	-146	0
-136	135	137	0
-136	-135	-137	0
-370	-371	413	0
-370	-369	411	0
-370	411	413	0
-370	-371	365	0
-370	-369	363	0
-370	363	365	0
-412	-413	371	0
-412	-411	369	0
-412	369	371	0
-412	-413	365	0
-412	-411	363	0
-412	363	365	0
-364	-365	371	0
-364	-363	369	0
-364	369	371	0
-364	-365	413	0
-364	-363	411	0
-364	411	413	0
-133	132	134	0
-133	-132	-134	0
-130	160	163	0
-163	162	164	0
-163	-162	-164	0
-160	159	161	0
-160	-159	-161	0
-343	-344	368	0
-343	-342	366	0
-343	366	368	0
-343	-344	359	0
-343	-342	357	0
-343	357	359	0
-343	-344	353	0
-343	-342	351	0
-343	351	353	0
-367	-368	344	0
-367	-366	342	0
-367	342	344	0
-367	-368	359	0
-367	-366	357	0
-367	357	359	0
-367	-368	353	0
-367	-366	351	0
-367	351	353	0
-358	-359	344	0
-358	-357	342	0
-358	342	344	0
-358	-359	368	0
-358	-357	366	0
-358	366	368	0
-358	-359	353	0
-358	-357	351	0
-358	351	353	0
-352	-353	344	0
-352	-351	342	0
-352	342	344	0
-352	-353	368	0
-352	-351	366	0
-352	366	368	0
-352	-353	359	0
-352	-351	357	0
-352	357	359	0
-130	129	131	0
-130	-129	-131	0
-343	342	344	0
-343	-342	-344	0
-172	171	173	0
-172	-171	-173	0
-154	153	155	0
-154	-153	-155	0
-151	150	152	0
-151	-150	-152	0
-127	126	128	0
-127	-126	-128	0
1034	48	-46	0
1035	-48	46	0
-1033	1035	1034	0
-154	-155	149	0
-154	-153	147	0
-154	147	149	0
-154	-155	167	0
-154	-153	165	0
-154	165	167	0
-154	-155	356	0
-154	-153	354	0
-154	354	356	0
-148	-149	155	0
-148	-147	153	0
-148	153	155	0
-148	-149	167	0
-148	-147	165	0
-148	165	167	0
-148	-149	356	0
-148	-147	354	0
-148	354	356	0
-166	-167	155	0
-166	-165	153	0
-166	153	155	0
-166	-167	149	0
-166	-165	147	0
-166	147	149	0
-166	-167	356	0
-166	-165	354	0
-166	354	356	0
-355	-356	155	0
-355	-354	153	0
-355	153	155	0
-355	-356	149	0
-355	-354	147	0
-355	147	149	0
-355	-356	167	0
-355	-354	165	0
-355	165	167	0
-47	46	48	0
-47	-46	-48	0
-142	166	169	0
-169	168	170	0
-169	-168	-170	0
-166	165	167	0
-166	-165	-167	0
-142	141	143	0
-142	-141	-143	0
372	378	381	0
-382	-383	-378	0
-382	-381	-380	0
-382	-378	-380	0
-379	-380	-381	0
-379	-378	-383	0
-379	-381	-383	0
-373	372	374	0
-373	-372	-374	0
374	380	383	0
1037	54	-52	0
1038	-54	52	0
-1036	1038	1037	0
-172	-173	158	0
-172	-171	156	0
-172	156	158	0
-172	-173	170	0
-172	-171	168	0
-172	168	170	0
-172	-173	164	0
-172	-171	162	0
-172	162	164	0
-157	-158	173	0
-157	-156	171	0
-157	171	173	0
-157	-158	170	0
-157	-156	168	0
-157	168	170	0
-157	-158	164	0
-157	-156	162	0
-157	162	164	0
-169	-170	173	0
-169	-168	171	0
-169	171	173	0
-169	-170	158	0
-169	-168	156	0
-169	156	158	0
-169	-170	164	0
-169	-168	162	0
-169	162	164	0
-163	-164	173	0
-163	-162	171	0
-163	171	173	0
-163	-164	158	0
-163	-162	156	0
-163	156	158	0
-163	-164	170	0
-163	-162	168	0
-163	168	170	0
-53	52	54	0
-53	-52	-54	0
-409	-410	404	0
-409	-408	402	0
-409	402	404	0
-409	-410	432	0
-409	-408	430	0
-409	430	432	0
-409	-410	401	0
-409	-408	399	0
-409	399	401	0
-403	-404	410	0
-403	-402	408	0
-403	408	410	0
-403	-404	432	0
-403	-402	430	0
-403	430	432	0
-403	-404	401	0
-403	-402	399	0
-403	399	401	0
-431	-432	410	0
-431	-430	408	0
-431	408	410	0
-431	-432	404	0
-431	-430	402	0
-431	402	404	0
-431	-432	401	0
-431	-430	399	0
-431	399	401	0
-400	-401	410	0
-400	-399	408	0
-400	408	410	0
-400	-401	404	0
-400	-399	402	0
-400	402	404	0
-400	-401	432	0
-400	-399	430	0
-400	430	432	0
-157	156	158	0
-157	-156	-158	0
669	665	667	706	0
-993	855	915	950	0
663	667	665	669	0
-665	-796	-781	-797	0
-196	658	661	677	0
268	498	489	493	0
270	500	489	493	0
446	458	787	679	0
448	460	789	681	0
-453	680	683	822	0
452	952	937	941	0
454	954	937	941	0
449	806	897	917	0
451	808	897	917	0
217	227	442	233	0
219	229	442	233	0
581	645	607	592	0
583	647	607	592	0
-118	334	337	519	0
117	530	554	534	0
119	532	554	534	0
-115	304	307	313	0
114	694	742	698	0
116	696	742	698	0
111	842	864	848	0
113	844	864	848	0
84	712	768	718	0
86	714	768	718	0
-248	559	562	625	0
-102	-75	-105	-90	0
-104	-77	-107	-92	0
-100	99	-96	-93	0
-100	101	-98	-95	0
524	527	515	99	0
524	527	327	99	0
-525	524	-327	-515	0
-525	526	-329	-517	0
-528	527	-327	-515	0
-528	529	-329	-517	0
524	529	517	101	0
524	529	329	101	0
96	845	874	849	0
98	847	874	849	0
105	241	221	244	0
107	243	223	246	0
800	809	784	244	0
800	811	786	246	0
-834	-833	818	670	0
-834	-835	820	672	0
833	955	961	962	0
835	957	961	962	0
-281	280	-277	-265	0
-281	282	-279	-267	0
631	648	611	280	0
631	648	642	280	0
-632	631	-642	-611	0
-632	633	-644	-613	0
-649	648	-642	-611	0
-649	650	-644	-613	0
631	650	613	282	0
631	650	644	282	0
277	501	507	508	0
279	503	507	508	0
-70	69	-81	-78	0
-70	71	-83	-80	0
-298	-297	294	291	0
-298	-299	296	293	0
297	691	726	697	0
299	693	726	697	0
81	715	752	719	0
83	717	752	719	0
-187	376	379	397	0
746	756	749	186	0
746	756	753	186	0
-747	-753	-748	-749	0
-747	-753	-746	-751	0
-747	-753	-749	-751	0
-757	-753	-758	-749	0
-757	-753	-756	-751	0
-757	-753	-749	-751	0
748	756	751	188	0
748	756	753	188	0
-770	-886	-771	-762	0
-770	-886	-769	-764	0
-770	-886	-762	-764	0
-766	-886	-767	-762	0
-766	-886	-765	-764	0
-766	-886	-762	-764	0
-887	-769	-888	-765	0
-887	-769	-886	-767	0
-887	-769	-765	-767	0
-763	-769	-764	-765	0
-763	-769	-762	-767	0
-763	-769	-765	-767	0
851	861	854	538	0
851	865	854	538	0
851	861	858	538	0
851	865	858	538	0
-852	-865	-853	-861	0
-852	-865	-851	-863	0
-852	-865	-861	-863	0
-852	-858	-853	-854	0
-852	-858	-851	-856	0
-852	-858	-854	-856	0
-866	-858	-867	-854	0
-866	-858	-865	-856	0
-866	-858	-854	-856	0
-862	-858	-863	-854	0
-862	-858	-861	-856	0
-862	-858	-854	-856	0
-859	-865	-860	-861	0
-859	-865	-858	-863	0
-859	-865	-861	-863	0
-855	-865	-856	-861	0
-855	-865	-854	-863	0
-855	-865	-861	-863	0
853	863	856	540	0
853	865	856	540	0
853	863	858	540	0
853	865	858	540	0
-879	-875	-880	-871	0
-879	-875	-878	-873	0
-879	-875	-871	-873	0
-731	-727	-732	-723	0
-731	-727	-730	-725	0
-731	-727	-723	-725	0
-744	-881	-745	-736	0
-744	-881	-743	-738	0
-744	-881	-736	-738	0
-740	-881	-741	-736	0
-740	-881	-739	-738	0
-740	-881	-736	-738	0
-882	-743	-883	-739	0
-882	-743	-881	-741	0
-882	-743	-739	-741	0
-737	-743	-738	-739	0
-737	-743	-736	-741	0
-737	-743	-739	-741	0
-180	-393	-384	-405	0
-182	-395	-386	-407	0
594	604	597	360	0
594	608	597	360	0
594	604	601	360	0
594	608	601	360	0
-595	-608	-596	-604	0
-595	-608	-594	-606	0
-595	-608	-604	-606	0
-595	-601	-596	-597	0
-595	-601	-594	-599	0
-595	-601	-597	-599	0
-609	-601	-610	-597	0
-609	-601	-608	-599	0
-609	-601	-597	-599	0
-605	-601	-606	-597	0
-605	-601	-604	-599	0
-605	-601	-597	-599	0
-602	-608	-603	-604	0
-602	-608	-601	-606	0
-602	-608	-604	-606	0
-598	-608	-599	-604	0
-598	-608	-597	-606	0
-598	-608	-604	-606	0
596	606	599	362	0
596	608	599	362	0
596	606	601	362	0
596	608	601	362	0
-629	634	-630	626	0
-629	634	-628	624	0
-629	634	624	626	0
-434	433	-417	-427	0
-434	435	-419	-429	0
256	262	259	253	0
256	486	259	253	0
256	262	509	253	0
256	486	509	253	0
-257	-486	-258	-262	0
-257	-486	-256	-264	0
-257	-486	-262	-264	0
-257	-509	-258	-259	0
-257	-509	-256	-261	0
-257	-509	-259	-261	0
-487	-509	-488	-259	0
-487	-509	-486	-261	0
-487	-509	-259	-261	0
-263	-509	-264	-259	0
-263	-509	-262	-261	0
-263	-509	-259	-261	0
-510	-486	-511	-262	0
-510	-486	-509	-264	0
-510	-486	-262	-264	0
-260	-486	-261	-262	0
-260	-486	-259	-264	0
-260	-486	-262	-264	0
258	264	261	255	0
258	486	261	255	0
258	264	509	255	0
258	486	509	255	0
-491	-504	-492	-474	0
-491	-504	-490	-476	0
-491	-504	-474	-476	0
-425	-421	-426	-471	0
-425	-421	-424	-473	0
-425	-421	-471	-473	0
-444	-772	-445	-436	0
-444	-772	-443	-438	0
-444	-772	-436	-438	0
-440	-772	-441	-436	0
-440	-772	-439	-438	0
-440	-772	-436	-438	0
-773	-443	-774	-439	0
-773	-443	-772	-441	0
-773	-443	-439	-441	0
-437	-443	-438	-439	0
-437	-443	-436	-441	0
-437	-443	-439	-441	0
-541	-568	-561	-345	0
-541	-568	-565	-345	0
-542	565	-543	563	0
-542	565	-541	561	0
-542	565	561	563	0
-569	565	-570	563	0
-569	565	-568	561	0
-569	565	561	563	0
-543	-568	-563	-347	0
-543	-568	-565	-347	0
-556	-548	-557	-544	0
-556	-548	-555	-546	0
-556	-548	-544	-546	0
-552	-548	-553	-544	0
-552	-548	-551	-546	0
-552	-548	-544	-546	0
-549	-555	-550	-551	0
-549	-555	-548	-553	0
-549	-555	-551	-553	0
-545	-555	-546	-551	0
-545	-555	-544	-553	0
-545	-555	-551	-553	0
812	830	827	177	0
812	934	827	177	0
812	830	942	177	0
812	934	942	177	0
-813	-934	-814	-830	0
-813	-934	-812	-832	0
-813	-934	-830	-832	0
-813	-942	-814	-827	0
-813	-942	-812	-829	0
-813	-942	-827	-829	0
-935	-942	-936	-827	0
-935	-942	-934	-829	0
-935	-942	-827	-829	0
-831	-942	-832	-827	0
-831	-942	-830	-829	0
-831	-942	-827	-829	0
-943	-934	-944	-830	0
-943	-934	-942	-832	0
-943	-934	-830	-832	0
-828	-934	-829	-830	0
-828	-934	-827	-832	0
-828	-934	-830	-832	0
814	832	829	179	0
814	934	829	179	0
814	832	942	179	0
814	934	942	179	0
-939	-958	-940	-928	0
-939	-958	-938	-930	0
-939	-958	-928	-930	0
918	911	921	198	0
918	911	914	198	0
-919	-921	-920	-914	0
-919	-921	-918	-916	0
-919	-921	-914	-916	0
-912	-921	-913	-914	0
-912	-921	-911	-916	0
-912	-921	-914	-916	0
918	913	921	200	0
918	913	916	200	0
-902	-905	-903	-894	0
-902	-905	-901	-896	0
-902	-905	-894	-896	0
-899	-905	-900	-894	0
-899	-905	-898	-896	0
-899	-905	-894	-896	0
-895	-898	-896	-901	0
-895	-898	-894	-903	0
-895	-898	-901	-903	0
-906	-898	-907	-901	0
-906	-898	-905	-903	0
-906	-898	-901	-903	0
-132	-363	-411	-369	0
-134	-365	-413	-371	0
-127	151	154	172	0
-1040	1019	994	987	0
-62	-699	-663	-65	-685	0
-64	-701	-663	-65	-685	0
-87	-108	-651	-446	-464	0
-89	-110	-653	-448	-466	0
108	123	318	303	333	0
110	125	320	305	335	0
-1022	750	872	895	929	0
221	224	230	420	234	0
223	226	232	420	234	0
174	189	180	183	375	0
176	191	182	185	377	0
-139	355	358	364	575	0
-49	-150	-159	-132	-144	0
-51	-152	-161	-134	-146	0
-136	145	148	352	400	0
-129	-351	-357	-366	-342	0
-131	-353	-359	-368	-344	0
-46	-354	-165	-147	-153	0
-48	-356	-167	-149	-155	0
-52	-162	-168	-156	-171	0
-54	-164	-170	-158	-173	0
-156	-399	-430	-402	-408	0
-158	-401	-432	-404	-410	0
53	47	50	56	44	986	0
-63	205	208	215	260	990	0
-990	289	437	496	545	991	0
-991	598	640	709	737	992	0
-992	763	779	828	839	993	0
-88	236	239	251	263	997	0
-997	272	310	316	325	998	0
-998	340	440	522	552	999	0
-999	605	621	740	766	1000	0
-1000	794	825	831	862	902	0
-103	472	475	578	724	1022	0
-349	367	370	382	403	572	0
-1039	1036	1033	1030	1027	1040	0";

            var solution = CNFSatSolver.SolveCNFString(problem, 5);

            Console.WriteLine(solution);

        }


        [TestMethod]
        public void OrderDeleteTupleVariablesByIndex()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new[] { 3, 2, -1 });
            solver.AddClause(new[] { -4, -3, 1 });

            var deleteCount = solver.DeletedTuples.Count;

            Assert.AreEqual(2, deleteCount, "Should have 2 deletes");

            foreach (var dt in solver.DeletedTuples)
            {
                int k = solver.VariablesUsed.Count;
                for (int i = 0; i < dt.AssignItems.Count; i++)
                {
                    var asx = dt.AssignItems[i];
                    Assert.IsTrue(asx.Index <= k, "Tuples should be in reverse column index order to support optimization" );
                    k = asx.Index;
                }
            }
        }

        [TestMethod]
        public void GetNextMatchingRanges()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new[] { 1, 2, 3, 4, 5, 6, 7, 8 });

            solver.Optimize();

            for (int i = 1; i < 7; i++)
            {
                solver.GetNextMatchingRange(3, 0, 0);
            }

        }

        [TestMethod]
        public void CountBitRowsTests()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new[] { 1, 2, 3, 4, 5, 6, 7 });

            Range r1 = new Range { Empty = false, Start = 0, Stop = 128 };
            Range r2 = new Range { Empty = false, Start = 0, Stop = 64 };
            Range r3 = new Range { Empty = false, Start = 0, Stop = 32 };
            Range r4 = new Range { Empty = false, Start = 0, Stop = 16 };
            Range r5 = new Range { Empty = false, Start = 64, Stop = 128 };
            Range r6 = new Range { Empty = false, Start = 0, Stop = 32 };
            Range r7 = new Range { Empty = false, Start = 32, Stop = 64 };
            Range r8 = new Range { Empty = false, Start = 4, Stop = 8 };

            BigInteger bi = 0;
            bi = solver.CountBitRows(1, 0, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(1, 1, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(2, 0, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(2, 1, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(3, 0, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(3, 1, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(7, 0, r1);
            Assert.IsTrue(bi == 64);
            bi = solver.CountBitRows(7, 1, r1);
            Assert.IsTrue(bi == 64);

            bi = solver.CountBitRows(1, 0, r8);
            Assert.IsTrue(bi == 2);
            bi = solver.CountBitRows(1, 1, r8);
            Assert.IsTrue(bi == 2);
            bi = solver.CountBitRows(2, 0, r8);
            Assert.IsTrue(bi == 2);
            bi = solver.CountBitRows(2, 1, r8);
            Assert.IsTrue(bi == 2);
            bi = solver.CountBitRows(3, 0, r8);
            Assert.IsTrue(bi == 0);
            bi = solver.CountBitRows(3, 1, r8);
            Assert.IsTrue(bi == 4);
            bi = solver.CountBitRows(7, 0, r8);
            Assert.IsTrue(bi == 4);
            bi = solver.CountBitRows(7, 1, r8);
            Assert.IsTrue(bi == 0);


            bi = solver.CountBitRows(4, 0, r4);
            Assert.IsTrue(bi == 8);
            bi = solver.CountBitRows(4, 1, r4);
            Assert.IsTrue(bi == 8);
        }

        [TestMethod]
        public void CountRowsTests()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause(new[] { 1, 2, 3, 4, 5, 6, 7, 8 });

            OverSATbLib.Tuple asn1 = new OverSATbLib.Tuple(1, 1);
            OverSATbLib.Tuple asn2 = new OverSATbLib.Tuple(1, 1, 2, 1);
            OverSATbLib.Tuple asn3 = new OverSATbLib.Tuple(1, 1, 2, 1, 3, 1);
            OverSATbLib.Tuple asn4 = new OverSATbLib.Tuple(1, 0, 2, 0, 3, 0);
            OverSATbLib.Tuple asn5 = new OverSATbLib.Tuple(4, 0);
            OverSATbLib.Tuple asn6 = new OverSATbLib.Tuple(8, 0);
            OverSATbLib.Tuple asn7 = new OverSATbLib.Tuple(4, 1);
            OverSATbLib.Tuple asn8 = new OverSATbLib.Tuple(8, 1);
            OverSATbLib.Tuple asn9 = new OverSATbLib.Tuple(1, 1, 8, 1);
            OverSATbLib.Tuple asn10 = new OverSATbLib.Tuple();
            OverSATbLib.Tuple asn11 = new OverSATbLib.Tuple();
            OverSATbLib.Tuple asn12 = new OverSATbLib.Tuple();

            for (int i = 1; i <= 8; i++)
            {
                asn10.AssignItems.Add(new Assignment { NameId = i, Value = 0 });
                asn11.AssignItems.Add(new Assignment { NameId = i, Value = (i > 4) ? 1u : 0u });
                asn12.AssignItems.Add(new Assignment { NameId = i, Value = 1 });
            }

            // RegisterTuple maps the indeces of the tuple so that 
            // count and other solver functions can work
            solver.RegisterTuple(asn1);
            solver.RegisterTuple(asn2);
            solver.RegisterTuple(asn3);
            solver.RegisterTuple(asn4);
            solver.RegisterTuple(asn5);
            solver.RegisterTuple(asn6);
            solver.RegisterTuple(asn7);
            solver.RegisterTuple(asn8);
            solver.RegisterTuple(asn9);
            solver.RegisterTuple(asn10);
            solver.RegisterTuple(asn11);
            solver.RegisterTuple(asn12);

            Range entireTable = new Range(0, solver.TotalRows);

            var count3 = solver.CountRows(asn3, entireTable);
            Assert.IsTrue(count3 == 32, "Should be 32 A=1,B=1,C=1");

            Range partialTable = new Range(0, 4);
            var count19= solver.CountRows(asn6, partialTable);
            Assert.IsTrue(count19 == 4, "Should be 4 A=1");

            var count1 = solver.CountRows(asn1, entireTable);
            Assert.IsTrue(count1 == 128, "Should be 128 A=1");

            var count2 = solver.CountRows(asn2, entireTable);
            Assert.IsTrue(count2 == 64, "Should be 64 A=1,B=1");

            var count4 = solver.CountRows(asn4, entireTable);
            Assert.IsTrue(count4 == 32, "Should be 32 A=0,B=0,C=0");

            var count5 = solver.CountRows(asn5, entireTable);
            Assert.IsTrue(count5 == 128, "Should be 128 D=0");
            var count6 = solver.CountRows(asn6, entireTable);
            Assert.IsTrue(count6 == 128, "Should be 128 H=0");
            var count7 = solver.CountRows(asn7, entireTable);
            Assert.IsTrue(count7 == 128, "Should be 128 D=1");
            var count8 = solver.CountRows(asn8, entireTable);
            Assert.IsTrue(count8 == 128, "Should be 128 H=1");
            var count9 = solver.CountRows(asn9, entireTable);
            Assert.IsTrue(count9 == 64, "Should be 64 H=1, A=1");
            var count10 = solver.CountRows(asn10, entireTable);
            Assert.IsTrue(count10 == 1, "Should be 1, A-H0");
            var count11 = solver.CountRows(asn11, entireTable);
            Assert.IsTrue(count11 == 1, "Should be 1, A-D1,E-H0");
            var count12 = solver.CountRows(asn12, entireTable);
            Assert.IsTrue(count12 == 1, "Should be 1, A-H0");

        }

        [TestMethod]
        public void CompareCounts()
        {
            SatSolver solver = new SatSolver();
            solver.AddClause(new[] { 1, 2, 3, 4, 5, 6, 7 });

            OverSATbLib.Tuple tx = new OverSATbLib.Tuple(4, 1, 3, 0, 2, 0, 1, 0);
            solver.RegisterTuple(tx);
            var txcount1 = solver.CountRows(tx, new Range { Start = 24, Stop = 28, Empty = false });
            Assert.IsTrue(txcount1 == 1);

            for (int c = 0; c < 128; c++)
            {
                OverSATbLib.Tuple t = new OverSATbLib.Tuple();

                int j = 1;
                for (int k = 0; k < 7; k++)
                {
                    if ((j & c) > 0)
                    {
                        t.AssignItems.Add(new Assignment { NameId = k+1, Value = 1 });
                    }
                    j <<= 1;
                }

                if (t.AssignItems.Count > 0)
                {
                    solver.RegisterTuple(t);

                    System.Diagnostics.Debug.WriteLine("TestA:" + t.ToString());

                    BigInteger count1 = solver.CountRows(t, new Range { Start = 0, Stop = 128, Empty = false });
                    BigInteger count2 = solver.CountRowsBruteForce(t, new Range { Start = 0, Stop = 128, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");
                }
            }

            for (int c = 0; c < 128; c++)
            {
                OverSATbLib.Tuple t = new OverSATbLib.Tuple();
                int j = 1;
                for (int k = 0; k < 7; k++)
                {
                    if ((j & c) >  0u)
                    {
                        t.AssignItems.Add(new Assignment { NameId = k+1, Value = 0 });
                    }
                    j <<= 1;
                }

                if (t.AssignItems.Count > 0)
                {
                    solver.RegisterTuple(t);

                    System.Diagnostics.Debug.WriteLine("TestB:" + t.ToString());

                    BigInteger count1 = solver.CountRows(t, new Range { Start = 0, Stop = 128, Empty = false });
                    BigInteger count2 = solver.CountRowsBruteForce(t, new Range { Start = 0, Stop = 128, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");
                }
            }

            for (int c = 0; c < 128; c++)
            {
                OverSATbLib.Tuple t = new OverSATbLib.Tuple();
                int j = 1;
                for (int k = 0; k < 7; k++)
                {
                    if ((j & c) > 0u)
                    {
                        t.AssignItems.Add(new Assignment { NameId = k + 1, Value = 1 });
                    }
                    else if (j < c)
                    {
                        t.AssignItems.Add(new Assignment { NameId = k + 1, Value = 0 });
                    }
                    j <<= 1;
                }

                if (t.AssignItems.Count > 0)
                {
                    solver.RegisterTuple(t);

                    System.Diagnostics.Debug.WriteLine("TestC:" + t.ToString());

                    BigInteger count1 = solver.CountRows(t, new Range { Start = 0, Stop = 128, Empty = false });
                    BigInteger count2 = solver.CountRowsBruteForce(t, new Range { Start = 0, Stop = 128, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 64, Stop = 128, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 64, Stop = 128, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 0, Stop = 8, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 0, Stop = 8, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 4, Stop = 8, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 4, Stop = 8, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 12, Stop = 16, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 12, Stop = 16, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 0, Stop = 32, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 0, Stop = 32, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 16, Stop = 32, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 16, Stop = 32, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                    count1 = solver.CountRows(t, new Range { Start = 24, Stop = 28, Empty = false });
                    count2 = solver.CountRowsBruteForce(t, new Range { Start = 24, Stop = 28, Empty = false });
                    Assert.IsTrue(count1 == count2, "Row counts must be the same");

                }
            }

        }

        [TestMethod]
        public void FindTrueRanges()
        {
            SatSolver solver = new SatSolver();
            solver.AddClause(new[] { 1, 2, 3, 4, 5 });

            List<OverSATbLib.Tuple> tuples = new List<OverSATbLib.Tuple>();

            OverSATbLib.Tuple tupleA = new OverSATbLib.Tuple(5, 0);
            OverSATbLib.Tuple tupleB = new OverSATbLib.Tuple(5, 1, 3, 0);
            OverSATbLib.Tuple tupleC = new OverSATbLib.Tuple(3, 1, 2, 1);
            OverSATbLib.Tuple tupleD = new OverSATbLib.Tuple(4, 0, 1, 1);
            OverSATbLib.Tuple tupleE = new OverSATbLib.Tuple(4, 1, 2, 1);
            OverSATbLib.Tuple tupleF = new OverSATbLib.Tuple(5, 0, 3, 0);

            /*******************************************

the problem is 4=1, 2=1

*****/


            tuples.Add( tupleA );
            tuples.Add( tupleB );
            tuples.Add( tupleC );
            tuples.Add( tupleD );
            tuples.Add( tupleE );
            tuples.Add( tupleF );

            foreach (var t in tuples)
            {
                solver.DeleteTuple(t);
            }

            solver.Optimize();

            var request = new SatSolver.TestRangeRequest();
            request.DeletedTuples = solver.DeletedTuples;
            request.Range = new Range();

            request.Range.Start = 0;
            request.Range.Stop = 16;
            var response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 0;
            request.Range.Stop = 8;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 8;
            request.Range.Stop = 16;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 0;
            request.Range.Stop = 4;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 4;
            request.Range.Stop = 8;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 16;
            request.Range.Stop = 32;
            response = solver.TestRange(request);
            Assert.IsTrue(response.HasTrues);
            Assert.IsTrue(!response.NewDeletedTuples.Any(a => a == tupleA));

            request.Range.Start = 16;
            request.Range.Stop = 24;
            response = solver.TestRange(request);
            Assert.IsTrue(response.HasTrues);

            request.Range.Start = 24;
            request.Range.Stop = 28;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);

            request.Range.Start = 24;
            request.Range.Stop = 32;
            response = solver.TestRange(request);
            Assert.IsTrue(response.HasTrues);

            request.Range.Start = 28;
            request.Range.Stop = 29;
            response = solver.TestRange(request);
            Assert.IsTrue(response.HasTrues);

            request.Range.Start = 30;
            request.Range.Stop = 32;
            response = solver.TestRange(request);
            Assert.IsFalse(response.HasTrues);
        }

    }

}
